diff -r 5a7194eeb4ed -r e95e212512d1 src/Tools/make-all-nj
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/make-all-nj	Fri May 13 11:10:14 1994 +0200
@@ -0,0 +1,8 @@
+#! /bin/sh
+#Make entire system using Standard ML of New Jersey
+#Pathnames will have to be modified for your site
+ISABELLEBIN=/homes/`whoami`/bin
+ISABELLECOMP=sml
+ISABELLEMAKE=Makefile.NJ
+export ISABELLEBIN ISABELLECOMP ISABELLEMAKE
+nohup make-all $*