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 $*