# HG changeset patch
# User wenzelm
# Date 1456177477 -3600
# Node ID 10e55e168672de93d8281136c27a847db77775d9
# Parent  340738057c8cf868f7a228e56da4910c43f179d8
avoid outdated Process.interruptConsoleProcesses;

diff -r 340738057c8c -r 10e55e168672 lib/scripts/run-polyml-5.6
--- a/lib/scripts/run-polyml-5.6	Mon Feb 22 14:37:56 2016 +0000
+++ b/lib/scripts/run-polyml-5.6	Mon Feb 22 22:44:37 2016 +0100
@@ -63,7 +63,7 @@
   esac
 else
   check_file "$INFILE"
-  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$PLATFORM_INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.success));"
+  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Thread.Thread.broadcastInterrupt ())); PolyML.SaveState.loadState \"$PLATFORM_INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.success));"
   EXIT=""
 fi