src/Tools/make-all-nj

--- a/src/Tools/make-all-nj	Mon Sep 29 15:08:47 1997 +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 $*