# HG changeset patch
# User wenzelm
# Date 1204831071 -3600
# Node ID e557c20158e20d6af91dd70ca143ea84482c80ca
# Parent  d34b68c21f9a8e3c74236ad349ac57667d644dea
system_out: threaded version does not work for 5.1;

diff -r d34b68c21f9a -r e557c20158e2 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Mar 06 20:17:50 2008 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Mar 06 20:17:51 2008 +0100
@@ -122,7 +122,7 @@
 
 (* system shell processes, with propagation of interrupts *)
 
-fun system_out script = uninterruptible (fn restore_attributes => fn () =>
+fun system_out_threaded script = uninterruptible (fn restore_attributes => fn () =>
   let
     val script_name = OS.FileSys.tmpName ();
     val _ = write_file script_name script;
@@ -183,6 +183,10 @@
     val rc = (case ! result of Signal => raise Interrupt | Result rc => rc);
   in (output, rc) end) ();
 
+val system_out =
+  if ml_system = "polyml-5.1" then system_out  (*signals not propagated from root thread!*)
+  else system_out_threaded;
+
 
 (* critical section -- may be nested within the same thread *)