Remove now-unused files

diff --git a/driver/ghci/ghci.sh b/driver/ghci/ghci.sh
deleted file mode 100644 (file)
index b020047..0000000
--- 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 (file)
index 10488b8..0000000
--- a/driver/ghci/ghcii.sh
+++ /dev/null
@@ -1,3 +0,0 @@
-#!/bin/sh
-# Mini-driver for GHCi
-exec "$0"/../ghc --interactive ${1+"$@"}