# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1711039010 -3600
# Node ID bc39a468ace6e979f973d919aa6c99c2efc56e9c
# Parent  8fe1ed4b5705f36aebd8edcde2b7ee7689fda2b5
raise error if benchmarking fails;

diff -r 8fe1ed4b5705 -r bc39a468ace6 src/Pure/Build/build_benchmark.scala
--- a/src/Pure/Build/build_benchmark.scala	Thu Mar 21 16:35:55 2024 +0100
+++ b/src/Pure/Build/build_benchmark.scala	Thu Mar 21 17:36:50 2024 +0100
@@ -120,7 +120,9 @@
       val deps0 = Sessions.deps(Sessions.load_structure(options))
       val build_context = Build.Context(store, deps0, build_hosts = build_hosts)
 
-      Build_Cluster.make(build_context, progress).open().init().benchmark().stop()
+      val build_cluster = Build_Cluster.make(build_context, progress).open().init().benchmark()
+      if (!build_cluster.ok) error("Benchmarking failed")
+      build_cluster.stop()
 
       using(store.open_server()) { server =>
         val db = store.open_build_database(path = Host.private_data.database, server = server)