proper order of modes;
authorwenzelm
Mon Dec 04 23:21:09 2000 +0100 (2000-12-04)
changeset 1058558a1ed1edb65
parent 10584 38e626f7dfa9
child 10586 b3f386ec0fd2
proper order of modes;
bin/isabelle
lib/Tools/usedir
     1.1 --- a/bin/isabelle	Mon Dec 04 23:20:37 2000 +0100
     1.2 +++ b/bin/isabelle	Mon Dec 04 23:21:09 2000 +0100
     1.3 @@ -86,7 +86,7 @@
     1.4        if [ -z "$MODES" ]; then
     1.5          MODES="\"$OPTARG\""
     1.6        else
     1.7 -        MODES="$MODES, \"$OPTARG\""
     1.8 +        MODES="\"$OPTARG\", $MODES"
     1.9        fi
    1.10        ;;
    1.11      q)
     2.1 --- a/lib/Tools/usedir	Mon Dec 04 23:20:37 2000 +0100
     2.2 +++ b/lib/Tools/usedir	Mon Dec 04 23:21:09 2000 +0100
     2.3 @@ -78,7 +78,7 @@
     2.4          if [ -z "$MODES" ]; then
     2.5            MODES="\"$OPTARG\""
     2.6          else
     2.7 -          MODES="$MODES, \"$OPTARG\""
     2.8 +          MODES="\"$OPTARG\", $MODES"
     2.9          fi
    2.10          ;;
    2.11        r)