make-all-nj

--- a/make-all-nj	Wed Jul 19 15:53:43 1995 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-#! /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
-export ISABELLEBIN ISABELLECOMP 
-nohup make-all $*