| changeset 2127 | 33f3d40145e8 |
| parent 2092 | 69bd90345078 |
| child 2216 | 9b080867c7b1 |
--- a/src/Tools/make-all Thu Oct 24 10:42:42 1996 +0200 +++ b/src/Tools/make-all Thu Oct 24 10:43:38 1996 +0200 @@ -19,7 +19,7 @@ # A typical shell script for /bin/sh is... # ML_DBASE=/usr/groups/theory/poly2.04/`arch`/ML_dbase # ISABELLEBIN=/homes/`whoami`/bin -# ISABELLECOMP="poly -noDisplay" +# ISABELLECOMP="/usr/bin/poly -noDisplay" # export ML_DBASE ISABELLEBIN ISABELLECOMP # nohup make-all $*