src/Pure/Thy/present.ML
changeset 51419 5313abe76bd4
parent 51415 8a33d581718b
child 51567 a86c5e02ba58
     1.1 --- a/src/Pure/Thy/present.ML	Wed Mar 13 16:04:16 2013 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Wed Mar 13 16:57:05 2013 +0100
     1.3 @@ -36,7 +36,6 @@
     1.4  val html_path = html_ext o Path.basic;
     1.5  val index_path = Path.basic "index.html";
     1.6  val readme_html_path = Path.basic "README.html";
     1.7 -val readme_path = Path.basic "README";
     1.8  val documentN = "document";
     1.9  val document_path = Path.basic documentN;
    1.10  val doc_indexN = "session";
    1.11 @@ -241,10 +240,7 @@
    1.12             else (); [])
    1.13          else doc_variants;
    1.14  
    1.15 -      val readme =
    1.16 -        if File.exists readme_html_path then SOME readme_html_path
    1.17 -        else if File.exists readme_path then SOME readme_path
    1.18 -        else NONE;
    1.19 +      val readme = if File.exists readme_html_path then SOME readme_html_path else NONE;
    1.20  
    1.21        val docs =
    1.22          (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @