diff -r 38e626f7dfa9 -r 58a1ed1edb65 bin/isabelle --- a/bin/isabelle Mon Dec 04 23:20:37 2000 +0100 +++ b/bin/isabelle Mon Dec 04 23:21:09 2000 +0100 @@ -86,7 +86,7 @@ if [ -z "$MODES" ]; then MODES="\"$OPTARG\"" else - MODES="$MODES, \"$OPTARG\"" + MODES="\"$OPTARG\", $MODES" fi ;; q)