src/Pure/System/benchmark.scala
changeset 79617 cdb51c7225ad
parent 79602 9ba800f12785
child 79618 50376abd132d
--- a/src/Pure/System/benchmark.scala	Thu Feb 15 11:33:36 2024 +0100
+++ b/src/Pure/System/benchmark.scala	Thu Feb 15 12:18:25 2024 +0100
@@ -39,7 +39,7 @@
       using_optional(store.maybe_open_database_server(server = server)) { database_server =>
         val db = store.open_build_database(path = Host.private_data.database, server = server)
 
-        progress.echo("Starting benchmark...")
+        progress.echo("Starting benchmark ...")
         val selection = Sessions.Selection(sessions = List(benchmark_session))
         val full_sessions = Sessions.load_structure(options.int("threads") = 1)