# HG changeset patch # User wenzelm # Date 1239724051 -7200 # Node ID b2dee0d2b618a5d2bb7492f7ff2eb6f5a62e97af # Parent 0214d179c2beac350858169452365ebe82bc8818# Parent 28c7f7ba9f131420fb00e5c80066f849d554f0e4 merged diff -r 0214d179c2be -r b2dee0d2b618 Admin/MacOS/script --- a/Admin/MacOS/script Tue Apr 14 15:41:40 2009 +0200 +++ b/Admin/MacOS/script Tue Apr 14 17:47:31 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