--- a/lib/scripts/run-smlnj Fri Feb 14 15:13:32 1997 +0100
+++ b/lib/scripts/run-smlnj Fri Feb 14 15:16:21 1997 +0100
@@ -54,10 +54,13 @@
START_SML="$ML_HOME/sml $ML_OPTIONS $DB"
if [ -n "$TERMINATE" ]; then
- { echo "$MLTEXT"; echo "$MLEXIT" } | $START_SML
+ { echo "$MLTEXT" "$MLEXIT" } | $START_SML
+ RC=$?
+elif [ -z "$MLTEXT" ]; then
+ sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML"
RC=$?
else
- { echo "$MLTEXT"; $ISABELLE_HOME/lib/scripts/ucat; echo "$MLEXIT" } | $START_SML
+ sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML"
RC=$?
fi