equal
deleted
inserted
replaced
24 if [ -z "$INFILE" ]; then |
24 if [ -z "$INFILE" ]; then |
25 EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" |
25 EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" |
26 MLWORKS="mlworks-basis -tty" |
26 MLWORKS="mlworks-basis -tty" |
27 else |
27 else |
28 EXIT="" |
28 EXIT="" |
29 MLWORKS="mlimage -load \"$INFILE\" -tty" |
29 MLWORKS="mlimage -load $INFILE -tty" |
30 fi |
30 fi |
31 |
31 |
32 if [ -z "$OUTFILE" ]; then |
32 if [ -z "$OUTFILE" ]; then |
33 COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' |
33 COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' |
34 else |
34 else |
47 else |
47 else |
48 FEEDER_OPTS="-q" |
48 FEEDER_OPTS="-q" |
49 fi |
49 fi |
50 |
50 |
51 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
51 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
52 { read FPID; "$ML_HOME/$MLWORKS" $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
52 { read FPID; "$ML_HOME"/$MLWORKS $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
53 RC="$?" |
53 RC="$?" |
54 |
54 |
55 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
55 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
56 |
56 |
57 exit "$RC" |
57 exit "$RC" |