eliminated pointless warning (see a35af478aee4): empty 'document_files' means there is no document;
--- 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 =