# HG changeset patch
# User wenzelm
# Date 1672762884 -3600
# Node ID d8cdddf7b9a5cf7d62870044a3ddd64052471376
# Parent  f405fcc3db3383274df32c3c0dd501ff224ce7f3
avoid somewhat fragile Document.Node.Name.master_dir_path;

diff -r f405fcc3db33 -r d8cdddf7b9a5 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Jan 03 16:53:43 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Jan 03 17:21:24 2023 +0100
@@ -472,7 +472,7 @@
               val bad =
                 (for {
                   name <- proper_session_theories.iterator
-                  path = name.master_dir_path
+                  path = Path.explode(name.master_dir)
                   if !ok(path.canonical_file)
                   path1 = File.relative_path(info.dir.canonical, path).getOrElse(path)
                 } yield (path1, name)).toList