diff -r 23734672dc12 -r 2da262e85c4d make-all-poly --- a/make-all-poly Wed Nov 09 15:47:11 1994 +0100 +++ b/make-all-poly Thu Nov 10 11:06:44 1994 +0100 @@ -1,8 +1,9 @@ #! /bin/sh +#$Id$ #Make entire system using Poly/ML #Pathnames will have to be modified for your site -ML_DBASE=/usr/groups/theory/poly/`arch`/ML_dbase -ISABELLEBIN=/homes/`whoami`/bin +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 $*