Admin/isatest/isatest-annomaly
changeset 28500 4b79e5d3d0aa
parent 22638 7cea3e27d05f
child 28504 7ad7d7d6df47
--- a/Admin/isatest/isatest-annomaly	Sat Oct 04 16:05:08 2008 +0200
+++ b/Admin/isatest/isatest-annomaly	Sat Oct 04 16:05:09 2008 +0200
@@ -42,7 +42,7 @@
 ## main
 
 ISABELLE_HOME="$DISTPREFIX/Isabelle"
-ISATOOL="$ISABELLE_HOME/bin/isatool"
+ISABELLE_TOOL="$ISABELLE_HOME/bin/isatool"
 
 [ -d $ISABELLE_HOME ] || fail "$ISABELLE_HOME is not a directory."
 
@@ -73,7 +73,7 @@
 do
   ( cd "$ISABELLE_HOME/src/$L"; \
     cat ~/settings/annomaly >> $ISABELLE_HOME/etc/settings; \
-    "$ISATOOL" make || fail "isatool make for $L failed." )
+    "$ISABELLE_TOOL" make || fail "isabelle make for $L failed." )
 done