src/Tools/make-all-nj
changeset 547 23e30d32cd0d
parent 370 e95e212512d1
--- a/src/Tools/make-all-nj	Thu Aug 18 17:56:07 1994 +0200
+++ b/src/Tools/make-all-nj	Fri Aug 19 10:57:40 1994 +0200
@@ -3,6 +3,5 @@
 #Pathnames will have to be modified for your site
 ISABELLEBIN=/homes/`whoami`/bin
 ISABELLECOMP=sml
-ISABELLEMAKE=Makefile.NJ
-export ISABELLEBIN ISABELLECOMP ISABELLEMAKE
+export ISABELLEBIN ISABELLECOMP 
 nohup make-all $*