# HG changeset patch
# User wenzelm
# Date 1363190225 -3600
# Node ID 5313abe76bd447b59065bfb446b706f88425d69f
# Parent  7b8ce84033409a7bae1657ae9e4655e5b64e1f2b
include only README.html, not historic README, which tends towards surprises like src/HOL/SPARK/Examples/README;

diff -r 7b8ce8403340 -r 5313abe76bd4 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")]) @