lib/scripts/run-smlnj-0.93
changeset 3010 4be22c300966
parent 3007 e5efa177ee0c
child 3055 5da4afa207ad
equal deleted inserted replaced
3009:38c0b6dbd24f 3010:4be22c300966
    48 ## run it!
    48 ## run it!
    49 
    49 
    50 START_SML="$INFILE $ML_OPTIONS"
    50 START_SML="$INFILE $ML_OPTIONS"
    51 
    51 
    52 if [ -n "$TERMINATE" ]; then
    52 if [ -n "$TERMINATE" ]; then
    53   { echo "$MLTEXT" "$MLEXIT" } | $START_SML
    53   echo "$MLTEXT" "$MLEXIT" | $START_SML
    54   RC=$?
    54   RC=$?
    55 elif [ -z "$MLTEXT" ]; then
    55 elif [ -z "$MLTEXT" ]; then
    56   sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML"
    56   sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML"
    57   RC=$?
    57   RC=$?
    58 else
    58 else