diff options
| -rw-r--r-- | driver/ghci/ghci.sh | 2 | ||||
| -rw-r--r-- | driver/ghci/ghcii.sh | 3 |
2 files changed, 0 insertions, 5 deletions
diff --git a/driver/ghci/ghci.sh b/driver/ghci/ghci.sh deleted file mode 100644 index b0200477b8..0000000000 --- a/driver/ghci/ghci.sh +++ /dev/null @@ -1,2 +0,0 @@ -# Mini-driver for GHCi -exec $GHCBIN $TOPDIROPT --interactive ${1+"$@"} diff --git a/driver/ghci/ghcii.sh b/driver/ghci/ghcii.sh deleted file mode 100644 index 10488b8d5b..0000000000 --- a/driver/ghci/ghcii.sh +++ /dev/null @@ -1,3 +0,0 @@ -#!/bin/sh -# Mini-driver for GHCi -exec "$0"/../ghc --interactive ${1+"$@"} |