ignore error code for "isabelle worker" (in contrast to eff08c3f89fe): avoid confusing "failed to work" messages via Build_Cluster.start;
authorwenzelm
Mon, 08 Jul 2024 17:57:19 +0200
changeset 80527 f6a9271cb177
parent 80526 c8537bef99eb
child 80529 e066cc867115
ignore error code for "isabelle worker" (in contrast to eff08c3f89fe): avoid confusing "failed to work" messages via Build_Cluster.start;
src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Mon Jul 08 17:44:20 2024 +0200
+++ b/src/Pure/Build/build.scala	Mon Jul 08 17:57:19 2024 +0200
@@ -691,17 +691,14 @@
         else if (quiet) new Progress
         else new Console_Progress(verbose = verbose)
 
-      val results =
-        progress.interrupt_handler {
-          build_worker(options,
-            build_id = build_id,
-            progress = progress,
-            dirs = dirs.toList,
-            numa_shuffling = Host.numa_check(progress, numa_shuffling),
-            max_jobs = max_jobs)
-        }
-
-      if (!results.ok) sys.exit(results.rc)
+      progress.interrupt_handler {
+        build_worker(options,
+          build_id = build_id,
+          progress = progress,
+          dirs = dirs.toList,
+          numa_shuffling = Host.numa_check(progress, numa_shuffling),
+          max_jobs = max_jobs)
+      }
     })