# HG changeset patch
# User wenzelm
# Date 1707995905 -3600
# Node ID cdb51c7225ad30371d78bf945d06295e199ab860
# Parent  12bb31d015108c3f46ec39f07fe9ccb33c0c17fd
tuned message;

diff -r 12bb31d01510 -r cdb51c7225ad src/Pure/System/benchmark.scala
--- 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)