# HG changeset patch
# User wenzelm
# Date 1300643796 -3600
# Node ID 78bb3ec281c29f2e3259312d471d27d43dc83f36
# Parent  e06351ffb475825792d2f190385c0282ee0f66b4
tuned;

diff -r e06351ffb475 -r 78bb3ec281c2 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sun Mar 20 18:09:32 2011 +0100
+++ b/src/Pure/Thy/present.ML	Sun Mar 20 18:56:36 2011 +0100
@@ -292,7 +292,7 @@
 
       val (doc_prefix1, documents) =
         if doc = "" then (NONE, [])
-        else if not (File.exists document_path) then
+        else if not (can File.check_dir document_path) then
           (if verbose then Output.raw_stderr "Warning: missing document directory\n" else ();
             (NONE, []))
         else (SOME (Path.append html_prefix document_path, html_prefix),
@@ -314,7 +314,7 @@
         (Url.File index_path, session_name) docs (Url.explode "medium.html");
     in
       session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
-      info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
+        info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
       browser_info := init_browser_info remote_path path thys;
       add_html_index (0, index_text)
     end);