# HG changeset patch # User wenzelm # Date 1669890651 -3600 # Node ID 8f580e62ca6e4795d1139a3d79c9d849c4f044ea # Parent 0af64cc2eee9496e5f5e7dcf277a59314444da44 tuned message; diff -r 0af64cc2eee9 -r 8f580e62ca6e src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Wed Nov 30 22:07:59 2022 +0100 +++ b/src/Pure/Thy/sessions.scala Thu Dec 01 11:30:51 2022 +0100 @@ -1075,7 +1075,10 @@ def check_session_dir(dir: Path): Path = if (is_session_dir(dir)) File.pwd() + dir.expand - else error("Bad session root directory (missing ROOT or ROOTS): " + dir.expand.toString) + else { + error("Bad session root directory: " + dir.expand.toString + + "\n (missing \"ROOT\" or \"ROOTS\")") + } def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] = { val default_dirs = Components.directories().filter(is_session_dir)