make-all-poly

--- a/make-all-poly	Wed Jul 19 15:53:43 1995 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#! /bin/sh
-#$Id$
-#Make entire system using Poly/ML
-#Pathnames will have to be modified for your site
-ML_DBASE=/usr/groups/theory/poly/polyml/`arch`/ML_dbase
-ISABELLEBIN=/homes/`whoami`/dbases
-ISABELLECOMP="poly -noDisplay -h 15000"
-export ML_DBASE ISABELLEBIN ISABELLECOMP 
-nohup make-all $*