# HG changeset patch
# User wenzelm
# Date 1195555335 -3600
# Node ID c1be3072ea8f19a75cfc123c837bed1ae600f127
# Parent  01f3686f43044b1385a2216861d0e111586bbded
PolyML.SaveState.loadState: exit on failure;

diff -r 01f3686f4304 -r c1be3072ea8f lib/scripts/run-polyml-5.1
--- a/lib/scripts/run-polyml-5.1	Mon Nov 19 13:42:09 2007 +0100
+++ b/lib/scripts/run-polyml-5.1	Tue Nov 20 11:42:15 2007 +0100
@@ -48,7 +48,7 @@
   EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
 else
   check_file "$INFILE"
-  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\");"
+  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle Fail msg => (TextIO.output (TextIO.stdErr, msg ^ \"\\n\"); OS.Process.exit OS.Process.failure));"
   EXIT=""
 fi