diff options
| author | priesnit <priesnit@chalmers.se> | 2006-03-02 22:47:45 +0000 |
|---|---|---|
| committer | priesnit <priesnit@chalmers.se> | 2006-03-02 22:47:45 +0000 |
| commit | e6f115a3006a64930f4bfd889dd215074c862cbb (patch) | |
| tree | 3b0740b12f1ddaa1a7d0bbaf5486ccc66b264119 /src/Makefile | |
| parent | 434053ac2c3242cc98d72f8f9b1d29088009ce5a (diff) | |
continuation of environment variable patch
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 |