# 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)] =
   {