fixed order of multiple -m options;
authorwenzelm
Thu Feb 18 12:15:55 1999 +0100 (1999-02-18)
changeset 6286ce30e19af3df
parent 6285 112a15c311f0
child 6287 61904a3eafaa
fixed order of multiple -m options;
bin/isabelle
     1.1 --- a/bin/isabelle	Thu Feb 18 12:05:16 1999 +0100
     1.2 +++ b/bin/isabelle	Thu Feb 18 12:15:55 1999 +0100
     1.3 @@ -68,7 +68,7 @@
     1.4        if [ -z "$MODES" ]; then
     1.5          MODES="\"$OPTARG\""
     1.6        else
     1.7 -        MODES="\"$OPTARG\", $MODES"
     1.8 +        MODES="$MODES, \"$OPTARG\""
     1.9        fi
    1.10        ;;
    1.11      q)