# HG changeset patch
# User wenzelm
# Date 1259420065 -3600
# Node ID a5e6e849a0d885bdef8efc81f6aecaa4707ea77a
# Parent  7c1764342cc8c1fb510a95f7e9a345890bf03ea6
allow spaces within PROOFGENERAL_EMACS;

diff -r 7c1764342cc8 -r a5e6e849a0d8 Admin/MacOS/App1/script
--- a/Admin/MacOS/App1/script	Sat Nov 28 15:53:10 2009 +0100
+++ b/Admin/MacOS/App1/script	Sat Nov 28 15:54:25 2009 +0100
@@ -48,8 +48,9 @@
   /Applications/Emacs.app/Contents/MacOS/Emacs \
   "")"
 
+declare -a EMACS_OPTIONS=()
 if [ -n "$PROOFGENERAL_EMACS" ]; then
-  EMACS_OPTIONS="-p $PROOFGENERAL_EMACS"
+  EMACS_OPTIONS=(-p "$PROOFGENERAL_EMACS")
 fi
 
 
@@ -57,7 +58,7 @@
 
 OUTPUT="/tmp/isabelle$$.out"
 
-( "$ISABELLE_TOOL" emacs $EMACS_OPTIONS "$@" ) > "$OUTPUT" 2>&1
+( "$ISABELLE_TOOL" emacs "${EMACS_OPTIONS[@]}" "$@" ) > "$OUTPUT" 2>&1
 RC=$?
 
 if [ "$RC" != 0 ]; then