# HG changeset patch
# User wenzelm
# Date 1568301472 -7200
# Node ID 0fec12eabad0f2459e087d3c6a545626a00455f8
# Parent  41b5e515c238470f22cf41747d7969c3732405e4
session directories need to exist;

diff -r 41b5e515c238 -r 0fec12eabad0 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Sep 12 16:52:04 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Sep 12 17:17:52 2019 +0200
@@ -384,7 +384,9 @@
               val errs2 =
                 if (bad_dirs.isEmpty) Nil
                 else List("Implicit use of session directories: " + commas(bad_dirs))
-              errs1 ::: errs2
+              val errs3 = for (p <- info.dirs if !p.is_dir) yield "No such directory: " + p
+
+              errs1 ::: errs2 ::: errs3
             }
 
             val sources_errors =