diff -r d927beecedf8 -r 33f3d40145e8 src/Tools/make-all
--- 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 $*