diff options
Diffstat (limited to 'src/Makefile')
| -rw-r--r-- | src/Makefile | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/Makefile b/src/Makefile index e44173676..efe9757b6 100644 --- a/src/Makefile +++ b/src/Makefile @@ -1,3 +1,5 @@ +include config.mk + GHMAKE=ghc GHCI=ghci @@ -45,13 +47,13 @@ api: shell: $(GHMAKE) $(GHCFLAGS) $(GHCINCLUDE) --make Shell.hs clean: - rm -rf */*.o */*.hi *.o *.hi */*.ghi *.ghi *~ */*~ + -rm -rf */*.o */*.hi *.o *.hi */*.ghi *.ghi *~ */*~ hugs: hugs -h10M -P$(HUGSINCLUDE) ghci-nofud: $(GHCI) $(GHCFLAGS) $(GHCINCLUDENOFUD) today: - runhugs util/MkToday + util/mktoday.sh javac: cd java ; javac *.java ; cd .. help: @@ -61,3 +63,8 @@ help: tracing: $(GHMAKE) $(GHCFLAGS) -itrace $(GHCINCLUDENOFUD) --make GF.hs -o gf2 ; strip gf2 ; mv gf2 ../bin/ +distclean: clean + -rm -f config.status config.mk config.log + +install: + $(INSTALL) ../bin/gf2 $(bindir) |