# HG changeset patch
# User wenzelm
# Date 1290954875 -3600
# Node ID 21f7e8d66a393d2b1ef83f51a45d94282659619c
# Parent  aa533c5e3f486cb138dda9f6b9753b8aa505ae43
more conventional exception propagation -- taking into account Simple_Thread.fork wrapping;

diff -r aa533c5e3f48 -r 21f7e8d66a39 src/Pure/Concurrent/bash.ML
--- a/src/Pure/Concurrent/bash.ML	Sun Nov 28 15:28:48 2010 +0100
+++ b/src/Pure/Concurrent/bash.ML	Sun Nov 28 15:34:35 2010 +0100
@@ -36,7 +36,8 @@
               | Posix.Process.W_STOPPED s =>
                   Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
           in Synchronized.change result (K res) end
-          handle _ (*sic*) => Synchronized.change result (fn Wait => Signal | res => res)));
+          handle exn =>
+            (Synchronized.change result (fn Wait => Signal | res => res); reraise exn)));
 
     fun terminate () =
       let