eliminated pointless warning (see a35af478aee4): empty 'document_files' means there is no document;
authorwenzelm
Mon Oct 30 19:36:27 2017 +0100 (18 months ago)
changeset 66945b6f787a17fbe
parent 66944 05df740cb54b
child 66946 3d8fd98c7c86
eliminated pointless warning (see a35af478aee4): empty 'document_files' means there is no document;
src/Pure/Thy/present.ML
     1.1 --- a/src/Pure/Thy/present.ML	Mon Oct 30 19:19:24 2017 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Mon Oct 30 19:36:27 2017 +0100
     1.3 @@ -171,13 +171,7 @@
     1.4        val doc_output =
     1.5          if document_output = "" then NONE else SOME (Path.explode document_output);
     1.6  
     1.7 -      val documents =
     1.8 -        if doc = "" then []
     1.9 -        else if null doc_files andalso not (can File.check_dir document_path) then
    1.10 -          (if verbose then Output.physical_stderr "Warning: missing document directory\n"
    1.11 -           else (); [])
    1.12 -        else doc_variants;
    1.13 -
    1.14 +      val documents = if doc = "" orelse null doc_files then [] else doc_variants;
    1.15        val readme = if File.exists readme_html_path then SOME readme_html_path else NONE;
    1.16  
    1.17        val docs =