# HG changeset patch
# User wenzelm
# Date 1239724044 -7200
# Node ID 28c7f7ba9f131420fb00e5c80066f849d554f0e4
# Parent  d7cfcb9b5c7c1f651af6976a4cb72859beb8f5c8
actually invoke ISABELLE_TOOL;

diff -r d7cfcb9b5c7c -r 28c7f7ba9f13 Admin/MacOS/script
--- a/Admin/MacOS/script	Tue Apr 14 14:37:44 2009 +0200
+++ b/Admin/MacOS/script	Tue Apr 14 17:47:24 2009 +0200
@@ -57,7 +57,7 @@
 
 OUTPUT="/tmp/isabelle$$.out"
 
-( "$HOME/bin/isabelle" emacs "$@" ) > "$OUTPUT" 2>&1
+( "$ISABELLE_TOOL" emacs "$@" ) > "$OUTPUT" 2>&1
 RC=$?
 
 if [ "$RC" != 0 ]; then