--- 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)