more parallelism: avoid exhaustion of standard thread pool;
authorwenzelm
Tue, 09 Feb 2021 14:55:36 +0100
changeset 73244 5bded25065f8
parent 73237 3d805ab66a2f
child 73245 f69cbb59813e
more parallelism: avoid exhaustion of standard thread pool;
src/Pure/System/bash.ML
--- a/src/Pure/System/bash.ML	Mon Feb 08 20:56:12 2021 +0100
+++ b/src/Pure/System/bash.ML	Tue Feb 09 14:55:36 2021 +0100
@@ -184,7 +184,7 @@
   end);
 
 fun process_scala script =
-  Scala.function "bash_process"
+  Scala.function_thread "bash_process"
     ("export ISABELLE_TMP=" ^ string (getenv "ISABELLE_TMP") ^ "\n" ^ script)
   |> YXML.parse_body
   |>