# HG changeset patch
# User wenzelm
# Date 1221078576 -7200
# Node ID 3eaad200d67a5834e2d36cf89b0931c7557dc909
# Parent  c6dad24124f141ab4651e5f28d02b0a207f70c6f
future_schedule: uninterruptible join;

diff -r c6dad24124f1 -r 3eaad200d67a src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Sep 10 21:50:32 2008 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Sep 10 22:29:36 2008 +0200
@@ -331,7 +331,7 @@
       in (x, Symtab.update (name, Future.task_of x) tab) end;
 
     val exns = #1 (fold_map future tasks Symtab.empty)
-      |> Future.join_results
+      |> uninterruptible (fn _ => Future.join_results)
       |> map_filter Exn.get_exn;
   in
     if null exns then ()