author | wenzelm |
Mon, 05 Dec 2022 14:47:08 +0100 | |
changeset 76557 | 6dc213e7f664 |
parent 76556 | c7f3e94fce7b |
child 76558 | d6a2a8bc40e1 |
--- a/src/Pure/Tools/mkroot.scala Mon Dec 05 12:17:56 2022 +0100 +++ b/src/Pure/Tools/mkroot.scala Mon Dec 05 14:47:08 2022 +0100 @@ -41,7 +41,9 @@ val root_tex = session_dir + Path.explode("document/root.tex") - progress.echo("\nCreating session " + quote(name) + " in " + session_dir.absolute) + progress.echo( + (if (quiet) "" else "\n") + + "Creating session " + quote(name) + " in " + session_dir.absolute) /* ROOT */