include only README.html, not historic README, which tends towards surprises like src/HOL/SPARK/Examples/README;
authorwenzelm
Wed, 13 Mar 2013 16:57:05 +0100
changeset 51419 5313abe76bd4
parent 51418 7b8ce8403340
child 51420 9cf33e987f0b
include only README.html, not historic README, which tends towards surprises like src/HOL/SPARK/Examples/README;
src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Wed Mar 13 16:04:16 2013 +0100
+++ b/src/Pure/Thy/present.ML	Wed Mar 13 16:57:05 2013 +0100
@@ -36,7 +36,6 @@
 val html_path = html_ext o Path.basic;
 val index_path = Path.basic "index.html";
 val readme_html_path = Path.basic "README.html";
-val readme_path = Path.basic "README";
 val documentN = "document";
 val document_path = Path.basic documentN;
 val doc_indexN = "session";
@@ -241,10 +240,7 @@
            else (); [])
         else doc_variants;
 
-      val readme =
-        if File.exists readme_html_path then SOME readme_html_path
-        else if File.exists readme_path then SOME readme_path
-        else NONE;
+      val readme = if File.exists readme_html_path then SOME readme_html_path else NONE;
 
       val docs =
         (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @