diff -r b2dee0d2b618 -r b310beb36645 Admin/MacOS/script --- a/Admin/MacOS/script Tue Apr 14 17:47:31 2009 +0200 +++ b/Admin/MacOS/script Tue Apr 14 18:18:15 2009 +0200 @@ -49,7 +49,7 @@ "")" if [ -n "$PROOFGENERAL_EMACS" ]; then - PROOFGENERAL_OPTIONS="-p $PROOFGENERAL_EMACS $PROOFGENERAL_OPTIONS" + EMACS_OPTIONS="-p $PROOFGENERAL_EMACS" fi @@ -57,7 +57,7 @@ OUTPUT="/tmp/isabelle$$.out" -( "$ISABELLE_TOOL" emacs "$@" ) > "$OUTPUT" 2>&1 +( "$ISABELLE_TOOL" emacs $EMACS_OPTIONS "$@" ) > "$OUTPUT" 2>&1 RC=$? if [ "$RC" != 0 ]; then