Admin/MacOS/App1/script
changeset 41610 9f99196ebd9f
parent 33912 a5e6e849a0d8
child 41642 b9442d9ce7f5
equal deleted inserted replaced
41609:f471a2fb9a95 41610:9f99196ebd9f
    56 
    56 
    57 # run interface with error feedback
    57 # run interface with error feedback
    58 
    58 
    59 OUTPUT="/tmp/isabelle$$.out"
    59 OUTPUT="/tmp/isabelle$$.out"
    60 
    60 
       
    61 # ( "$ISABELLE_TOOL" jedit "$@" ) > "$OUTPUT" 2>&1
    61 ( "$ISABELLE_TOOL" emacs "${EMACS_OPTIONS[@]}" "$@" ) > "$OUTPUT" 2>&1
    62 ( "$ISABELLE_TOOL" emacs "${EMACS_OPTIONS[@]}" "$@" ) > "$OUTPUT" 2>&1
    62 RC=$?
    63 RC=$?
    63 
    64 
    64 if [ "$RC" != 0 ]; then
    65 if [ "$RC" != 0 ]; then
    65   echo >> "$OUTPUT"
    66   echo >> "$OUTPUT"