# HG changeset patch # User wenzelm # Date 1614429424 -3600 # Node ID 54262af6d310f7d3e886462e76c9b1d8e2afe2f3 # Parent 6e155bb1516d3683f8bbd6606c2729da3a09c1dd clarified message; diff -r 6e155bb1516d -r 54262af6d310 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Sat Feb 27 13:20:52 2021 +0100 +++ b/src/Pure/Thy/sessions.scala Sat Feb 27 13:37:04 2021 +0100 @@ -1013,7 +1013,7 @@ private def check_session_dir(dir: Path): Path = if (is_session_dir(dir)) File.pwd() + dir.expand - else error("Bad session root directory: " + dir.expand.toString) + else error("Bad session root directory (missing ROOT or ROOTS): " + dir.expand.toString) def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] = {