# 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);