bin/isabelle
changeset 2711 098f9ce0541a
parent 2704 afa01c9f1ab0
child 2735 29434f9b95dd
equal deleted inserted replaced
2710:3b26198fdaa5 2711:098f9ce0541a
    78       ;;
    78       ;;
    79     m)
    79     m)
    80       if [ -z "$MODES" ]; then
    80       if [ -z "$MODES" ]; then
    81         MODES="\"$OPTARG\""
    81         MODES="\"$OPTARG\""
    82       else
    82       else
    83         MODES="$MODES, \"$OPTARG\""
    83         MODES="\"$OPTARG\", $MODES"
    84       fi
    84       fi
    85       ;;
    85       ;;
    86     q)
    86     q)
    87       TERMINATE=true
    87       TERMINATE=true
    88       ;;
    88       ;;