# HG changeset patch # User wenzelm # Date 979601257 -3600 # Node ID e23abeef8150c51f8dca92e2809704a0b1d5642d # Parent 624077d5afddda4252395747cba7c017d9bbccd6 -f option; diff -r 624077d5afdd -r e23abeef8150 bin/isabelle --- a/bin/isabelle Tue Jan 16 00:25:54 2001 +0100 +++ b/bin/isabelle Tue Jan 16 00:27:37 2001 +0100 @@ -29,6 +29,7 @@ echo " -P startup Proof General interaction mode" echo " -c tell ML system to compress output image" echo " -e MLTEXT pass MLTEXT to the ML session" + echo " -f pass 'Session.finish();' to the ML session" echo " -m MODE add print mode for output" echo " -q non-interactive session" echo " -r open heap file read-only" @@ -64,7 +65,7 @@ READONLY="" NOWRITE="" -while getopts "CIPce:m:qruw" OPT +while getopts "CIPce:fm:qruw" OPT do case "$OPT" in C) @@ -82,6 +83,9 @@ e) MLTEXT="$MLTEXT $OPTARG" ;; + f) + MLTEXT="$MLTEXT Session.finish();" + ;; m) if [ -z "$MODES" ]; then MODES="\"$OPTARG\""