lib/scripts/run-smlnj
changeset 3010 4be22c300966
parent 3007 e5efa177ee0c
child 3046 6b7935317538
equal deleted inserted replaced
3009:38c0b6dbd24f 3010:4be22c300966
    52 ## run it!
    52 ## run it!
    53 
    53 
    54 START_SML="$ML_HOME/sml $ML_OPTIONS $DB"
    54 START_SML="$ML_HOME/sml $ML_OPTIONS $DB"
    55 
    55 
    56 if [ -n "$TERMINATE" ]; then
    56 if [ -n "$TERMINATE" ]; then
    57   { echo "$MLTEXT" "$MLEXIT" } | $START_SML
    57   echo "$MLTEXT" "$MLEXIT" | $START_SML
    58   RC=$?
    58   RC=$?
    59 elif [ -z "$MLTEXT" ]; then
    59 elif [ -z "$MLTEXT" ]; then
    60   sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML"
    60   sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML"
    61   RC=$?
    61   RC=$?
    62 else
    62 else