bin/isabelle
changeset 10585 58a1ed1edb65
parent 10555 2323ec838401
child 10905 e23abeef8150
equal deleted inserted replaced
10584:38e626f7dfa9 10585:58a1ed1edb65
    84       ;;
    84       ;;
    85     m)
    85     m)
    86       if [ -z "$MODES" ]; then
    86       if [ -z "$MODES" ]; then
    87         MODES="\"$OPTARG\""
    87         MODES="\"$OPTARG\""
    88       else
    88       else
    89         MODES="$MODES, \"$OPTARG\""
    89         MODES="\"$OPTARG\", $MODES"
    90       fi
    90       fi
    91       ;;
    91       ;;
    92     q)
    92     q)
    93       TERMINATE=true
    93       TERMINATE=true
    94       ;;
    94       ;;