# HG changeset patch
# User wenzelm
# Date 1509388587 -3600
# Node ID b6f787a17fbe18b0f4b3d12d0f0c2402b1087940
# Parent  05df740cb54b0585870109ad700f1a01536a9971
eliminated pointless warning (see a35af478aee4): empty 'document_files' means there is no document;

diff -r 05df740cb54b -r b6f787a17fbe src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Mon Oct 30 19:19:24 2017 +0100
+++ b/src/Pure/Thy/present.ML	Mon Oct 30 19:36:27 2017 +0100
@@ -171,13 +171,7 @@
       val doc_output =
         if document_output = "" then NONE else SOME (Path.explode document_output);
 
-      val documents =
-        if doc = "" then []
-        else if null doc_files andalso not (can File.check_dir document_path) then
-          (if verbose then Output.physical_stderr "Warning: missing document directory\n"
-           else (); [])
-        else doc_variants;
-
+      val documents = if doc = "" orelse null doc_files then [] else doc_variants;
       val readme = if File.exists readme_html_path then SOME readme_html_path else NONE;
 
       val docs =