# HG changeset patch
# User wenzelm
# Date 1291393013 -3600
# Node ID d9c112c587f9514e99cf6d97e196cd5dad453969
# Parent  c3f68ea9749512edc5e8d642d30e6e4de674f781
bash wrapper: terminate only in exceptional case, keep background processes running (e.g. 'thy_deps' or 'display_drafts');

diff -r c3f68ea97495 -r d9c112c587f9 src/Pure/Concurrent/bash.ML
--- a/src/Pure/Concurrent/bash.ML	Fri Dec 03 16:39:07 2010 +0100
+++ b/src/Pure/Concurrent/bash.ML	Fri Dec 03 17:16:53 2010 +0100
@@ -64,8 +64,7 @@
       in () end;
 
     fun cleanup () =
-     (terminate ();
-      Simple_Thread.interrupt system_thread;
+     (Simple_Thread.interrupt system_thread;
       try File.rm script_path;
       try File.rm output_path;
       try File.rm pid_path);
@@ -79,6 +78,6 @@
       val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
       val _ = cleanup ();
     in (output, rc) end
-    handle exn => (cleanup (); reraise exn)
+    handle exn => (terminate(); cleanup (); reraise exn)
   end);