1.1 --- a/lib/scripts/run-smlnj	Fri Feb 14 15:13:32 1997 +0100
     1.2 +++ b/lib/scripts/run-smlnj	Fri Feb 14 15:16:21 1997 +0100
     1.3 @@ -54,10 +54,13 @@
     1.4  START_SML="$ML_HOME/sml $ML_OPTIONS $DB"
     1.5  
     1.6  if [ -n "$TERMINATE" ]; then
     1.7 -  { echo "$MLTEXT"; echo "$MLEXIT" } | $START_SML
     1.8 +  { echo "$MLTEXT" "$MLEXIT" } | $START_SML
     1.9 +  RC=$?
    1.10 +elif [ -z "$MLTEXT" ]; then
    1.11 +  sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML"
    1.12    RC=$?
    1.13  else
    1.14 -  { echo "$MLTEXT"; $ISABELLE_HOME/lib/scripts/ucat; echo "$MLEXIT" } | $START_SML
    1.15 +  sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML"
    1.16    RC=$?
    1.17  fi
    1.18  

     2.1 --- a/lib/scripts/run-smlnj-0.93	Fri Feb 14 15:13:32 1997 +0100
     2.2 +++ b/lib/scripts/run-smlnj-0.93	Fri Feb 14 15:16:21 1997 +0100
     2.3 @@ -29,7 +29,7 @@
     2.4  MOVE=""
     2.5  
     2.6  if [ -z "$OUTFILE" ]; then
     2.7 -  COMMIT='fun commit () = (output (std_err, "Error - Database is not opened for writing.\n"); false);'
     2.8 +  COMMIT='fun commit () = (output (std_err, "Error - Database is not opened for writing.\\n"); false);'
     2.9  else
    2.10    if [ "$INFILE" -ef "$OUTFILE" ]; then
    2.11      OUTDIR=$(dirname "$OUTFILE")/tmp
    2.12 @@ -50,10 +50,13 @@
    2.13  START_SML="$INFILE $ML_OPTIONS"
    2.14  
    2.15  if [ -n "$TERMINATE" ]; then
    2.16 -  { echo "$MLTEXT"; echo "$MLEXIT" } | $START_SML
    2.17 +  { echo "$MLTEXT" "$MLEXIT" } | $START_SML
    2.18 +  RC=$?
    2.19 +elif [ -z "$MLTEXT" ]; then
    2.20 +  sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML"
    2.21    RC=$?
    2.22  else
    2.23 -  { echo "$MLTEXT"; $ISABELLE_HOME/lib/scripts/ucat; echo "$MLEXIT" } | $START_SML
    2.24 +  sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML"
    2.25    RC=$?
    2.26  fi
    2.27