# HG changeset patch
# User wenzelm
# Date 1420830762 -3600
# Node ID cb3a4caf206d4bee5cc3877450f103413fe9adde
# Parent  72278d083d3a2b03f9f2ccb9333b9f77755082ac
permissive worker_start: failure to fork thread is deferred to later attempt to provide missing threads, without crashing scheduler;

diff -r 72278d083d3a -r cb3a4caf206d src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Fri Jan 09 19:20:00 2015 +0100
+++ b/src/Pure/Concurrent/future.ML	Fri Jan 09 20:12:42 2015 +0100
@@ -264,7 +264,9 @@
 
 fun worker_start name = (*requires SYNCHRONIZED*)
   Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
-    Unsynchronized.ref Working));
+    Unsynchronized.ref Working))
+  handle Fail msg => Multithreading.tracing 0 (fn () => msg);
+
 
 
 (* scheduler *)