From ec0d525426207b8c1e6432bc7efe9d25c9ecf3c1 Mon Sep 17 00:00:00 2001 From: Makarius Date: Mon, 5 Dec 2022 15:21:26 +0100 Subject: [PATCH] Tuned messages, following Isabelle/d6a2a8bc40e1 --- src/scala/dof_mkroot.scala | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/scala/dof_mkroot.scala b/src/scala/dof_mkroot.scala index ad6992c..c600909 100644 --- a/src/scala/dof_mkroot.scala +++ b/src/scala/dof_mkroot.scala @@ -62,7 +62,9 @@ object DOF_Mkroot val document_path = session_dir + Path.explode("document") if (document_path.file.exists) error("Cannot overwrite existing " + document_path) - progress.echo("\nCreating session " + quote(name) + " in " + session_dir.absolute) + progress.echo( + (if (quiet) "" else "\n") + + "Initializing session " + quote(name) + " in " + session_dir.absolute) /* ROOT */ @@ -106,7 +108,8 @@ end /* Mercurial repository */ if (init_repos) { - progress.echo(" \nInitializing Mercurial repository " + session_dir) + progress.echo( + (if (quiet) "" else "\n") + "Initializing Mercurial repository " + session_dir.absolute) val hg = Mercurial.init_repository(session_dir)