# HG changeset patch
# User wenzelm
# Date 1289498117 -3600
# Node ID d695d258dfbcffdea2f3581a5a1783d60abecce5
# Parent  cc06f5528bb1a18c11ec70e3da12e4b26da0847e
tuned error message;

diff -r cc06f5528bb1 -r d695d258dfbc lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Thu Nov 11 17:07:05 2010 +0100
+++ b/lib/scripts/run-polyml	Thu Nov 11 18:55:17 2010 +0100
@@ -47,7 +47,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\" handle Fail msg => (TextIO.output (TextIO.stdErr, msg ^ \"\\n\"); OS.Process.exit OS.Process.failure));"
+  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle Fail msg => (TextIO.output (TextIO.stdErr, msg ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.failure));"
   EXIT=""
 fi
 
@@ -78,3 +78,5 @@
 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
 
 exit "$RC"
+
+#:wrap=soft:maxLineLen=100: