| changeset 3010 | 4be22c300966 |
| parent 3007 | e5efa177ee0c |
| child 3055 | 5da4afa207ad |
--- a/lib/scripts/run-smlnj-0.93 Tue Apr 22 11:49:55 1997 +0200 +++ b/lib/scripts/run-smlnj-0.93 Tue Apr 22 18:05:42 1997 +0200 @@ -50,7 +50,7 @@ START_SML="$INFILE $ML_OPTIONS" if [ -n "$TERMINATE" ]; then - { echo "$MLTEXT" "$MLEXIT" } | $START_SML + echo "$MLTEXT" "$MLEXIT" | $START_SML RC=$? elif [ -z "$MLTEXT" ]; then sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML"