Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
bash wrapper: terminate only in exceptional case, keep background processes running (e.g. 'thy_deps' or 'display_drafts');
authorwenzelm
Fri, 03 Dec 2010 17:16:53 +0100
changeset 40896 d9c112c587f9
parent 40895 c3f68ea97495
child 40935 f48c5b951042
bash wrapper: terminate only in exceptional case, keep background processes running (e.g. 'thy_deps' or 'display_drafts');
src/Pure/Concurrent/bash.ML file | annotate | diff | comparison | revisions 
--- 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);
isabelle