tuned messages;
authorwenzelm
Mon, 05 Dec 2022 15:19:52 +0100
changeset 76558 d6a2a8bc40e1
parent 76557 6dc213e7f664
child 76561 595261b3d033
child 76562 9c5780693350
tuned messages;
src/Pure/Tools/mkroot.scala
--- a/src/Pure/Tools/mkroot.scala	Mon Dec 05 14:47:08 2022 +0100
+++ b/src/Pure/Tools/mkroot.scala	Mon Dec 05 15:19:52 2022 +0100
@@ -43,7 +43,7 @@
 
     progress.echo(
       (if (quiet) "" else "\n") +
-      "Creating session " + quote(name) + " in " + session_dir.absolute)
+      "Initializing session " + quote(name) + " in " + session_dir.absolute)
 
 
     /* ROOT */
@@ -139,7 +139,9 @@
     /* Mercurial repository */
 
     if (init_repos) {
-      progress.echo_if(!quiet, "  \nInitializing Mercurial repository " + session_dir)
+      progress.echo(
+        (if (quiet) "" else "\n") +
+        "Initializing Mercurial repository " + session_dir.absolute)
 
       val hg = Mercurial.init_repository(session_dir)