# HG changeset patch
# User wenzelm
# Date 1374269383 -7200
# Node ID 43e48bb554ba43e02e2fbbc70669a0467a39cdfd
# Parent  155f02cacb2dec6b851a22d90c2e0c3a6d08c5ba
proper Future.shutdown, to wait for the scheduler thread to finish remaining tasks (notably external processes);

diff -r 155f02cacb2d -r 43e48bb554ba src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Fri Jul 19 20:56:39 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML	Fri Jul 19 23:29:43 2013 +0200
@@ -188,7 +188,7 @@
     | name :: args => (worker_guest (fn () => run_command name args); true))
     handle Runtime.TERMINATE => false
       | exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true);
-  in if continue then loop channel else () end;
+  in if continue then loop channel else Future.shutdown () end;
 
 end;