# HG changeset patch
# User wenzelm
# Date 1518438450 -3600
# Node ID 02cf352cbc4c2e89f9faf1941ec640af26877167
# Parent  686679dedb46d7a88b27f2a5c548190059ef2cea
permissive Doc.dirs: some entries may be absent due to distribution bootstrap, e.g. $JEDIT_HOME/dist/doc;

diff -r 686679dedb46 -r 02cf352cbc4c src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala	Sun Feb 11 22:26:58 2018 +0100
+++ b/src/Pure/Tools/doc.scala	Mon Feb 12 13:27:30 2018 +0100
@@ -15,9 +15,7 @@
   /* dirs */
 
   def dirs(): List[Path] =
-    Path.split(Isabelle_System.getenv("ISABELLE_DOCS")).map(dir =>
-      if (dir.is_dir) dir
-      else error("Bad documentation directory: " + dir))
+    Path.split(Isabelle_System.getenv("ISABELLE_DOCS"))
 
 
   /* contents */