equal
deleted
inserted
replaced
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"; echo "$MLEXIT" } | $START_SML |
57 { echo "$MLTEXT" "$MLEXIT" } | $START_SML |
|
58 RC=$? |
|
59 elif [ -z "$MLTEXT" ]; then |
|
60 sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML" |
58 RC=$? |
61 RC=$? |
59 else |
62 else |
60 { echo "$MLTEXT"; $ISABELLE_HOME/lib/scripts/ucat; echo "$MLEXIT" } | $START_SML |
63 sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML" |
61 RC=$? |
64 RC=$? |
62 fi |
65 fi |
63 |
66 |
64 exit $RC |
67 exit $RC |