diff options
Diffstat (limited to 'src/Makefile')
| -rw-r--r-- | src/Makefile | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Makefile b/src/Makefile index b59ff6676..22727ca87 100644 --- a/src/Makefile +++ b/src/Makefile @@ -110,6 +110,7 @@ clean: -rm -f JavaGUI/*.class -rm -f $(GFEDITOR)/de/uka/ilkd/key/ocl/gf/*.class -rm -f gf.wixobj + -rm -f ../bin/$(GF_EXE) distclean: clean -rm -f JavaGUI/gf-java.jar jgf @@ -254,6 +255,6 @@ install-editor: install-java: javac -rm -f ../bin/JavaGUI ln -s ../src/JavaGUI ../bin - @echo "PLEASE edit GFHOME in bin/jgf" + @echo "PLEASE set GFHOME and GF_LIB_PATH in your environment" -rm -f ../bin/$(GFEDITOR) ln -s ../src/$(GFEDITOR) ../bin |