From d7323c8812f2a07a3f3a334730cf18ec0f5d41a1 Mon Sep 17 00:00:00 2001 From: Ian Lynagh Date: Sat, 2 Jun 2007 12:11:59 +0000 Subject: [PATCH] Remove now-unused files --- driver/ghci/ghci.sh | 2 -- driver/ghci/ghcii.sh | 3 --- 2 files changed, 5 deletions(-) delete mode 100644 driver/ghci/ghci.sh delete mode 100644 driver/ghci/ghcii.sh diff --git a/driver/ghci/ghci.sh b/driver/ghci/ghci.sh deleted file mode 100644 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 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+"$@"} -- 1.7.10.4