--- a/bin/isabelle Mon Mar 03 14:14:04 1997 +0100 +++ b/bin/isabelle Mon Mar 03 18:24:34 1997 +0100 @@ -80,7 +80,7 @@ if [ -z "$MODES" ]; then MODES="\"$OPTARG\"" else - MODES="$MODES, \"$OPTARG\"" + MODES="\"$OPTARG\", $MODES" fi ;; q)