bin/isabelle
changeset 6286 ce30e19af3df
parent 5954 4ec8b8f957e6
child 7887 eedfff88ee40
equal deleted inserted replaced
6285:112a15c311f0 6286:ce30e19af3df
    66       ;;
    66       ;;
    67     m)
    67     m)
    68       if [ -z "$MODES" ]; then
    68       if [ -z "$MODES" ]; then
    69         MODES="\"$OPTARG\""
    69         MODES="\"$OPTARG\""
    70       else
    70       else
    71         MODES="\"$OPTARG\", $MODES"
    71         MODES="$MODES, \"$OPTARG\""
    72       fi
    72       fi
    73       ;;
    73       ;;
    74     q)
    74     q)
    75       TERMINATE=true
    75       TERMINATE=true
    76       ;;
    76       ;;