Delete libraries/ghci/GNUmakefile [skip ci]
authorThomas Miedema <thomasmiedema@gmail.com>
Tue, 17 May 2016 16:05:28 +0000 (18:05 +0200)
committerThomas Miedema <thomasmiedema@gmail.com>
Tue, 17 May 2016 16:06:05 +0000 (18:06 +0200)
This file should not have been included in the repository, as it is
generated by `./boot`.

libraries/ghci/GNUmakefile [deleted file]

diff --git a/libraries/ghci/GNUmakefile b/libraries/ghci/GNUmakefile
deleted file mode 100644 (file)
index ce6a24f..0000000
+++ /dev/null
@@ -1,4 +0,0 @@
-dir = libraries/ghci
-TOP = ../..
-include $(TOP)/mk/sub-makefile.mk
-FAST_MAKE_OPTS += stage=0