--- a/bin/isabelle Thu Feb 18 12:05:16 1999 +0100 +++ b/bin/isabelle Thu Feb 18 12:15:55 1999 +0100 @@ -68,7 +68,7 @@ if [ -z "$MODES" ]; then MODES="\"$OPTARG\"" else - MODES="\"$OPTARG\", $MODES" + MODES="$MODES, \"$OPTARG\"" fi ;; q)