diff --git a/build.sh b/build.sh old mode 100644 new mode 100755 diff --git a/cbt.sh b/cbt.sh old mode 100644 new mode 100755 diff --git a/clean.sh b/clean.sh old mode 100644 new mode 100755 diff --git a/db.sh b/db.sh old mode 100644 new mode 100755 diff --git a/ghci.sh b/ghci.sh old mode 100644 new mode 100755 diff --git a/hlint.sh b/hlint.sh old mode 100644 new mode 100755 diff --git a/hoogle.sh b/hoogle.sh old mode 100644 new mode 100755 diff --git a/is-clean.sh b/is-clean.sh old mode 100644 new mode 100755 diff --git a/load.sh b/load.sh old mode 100644 new mode 100755 diff --git a/missing-translations.sh b/missing-translations.sh old mode 100644 new mode 100755 diff --git a/run.sh b/run.sh deleted file mode 120000 index ebcc7e664..000000000 --- a/run.sh +++ /dev/null @@ -1 +0,0 @@ -start.sh \ No newline at end of file diff --git a/start.sh b/start.sh old mode 100644 new mode 100755 diff --git a/test.sh b/test.sh old mode 100644 new mode 100755 diff --git a/translate.hs b/translate.hs old mode 100644 new mode 100755