--- 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)