# HG changeset patch
# User wenzelm
# Date 876843405 -7200
# Node ID 86981c4bffdbbc6d68db4d7babe48e86457f724a
# Parent  3b2587c809f4bd3fccdefd6762ba50c076a273ab
tuned;

diff -r 3b2587c809f4 -r 86981c4bffdb src/Pure/Thy/browser_info.ML
--- a/src/Pure/Thy/browser_info.ML	Tue Oct 14 17:36:22 1997 +0200
+++ b/src/Pure/Thy/browser_info.ML	Tue Oct 14 17:36:45 1997 +0200
@@ -564,9 +564,9 @@
           else space_implode "/" (take (level, subdirs))))) ^
        "\n" ^
        (if file_exists (tack_on (!index_path) "README.html") then
-          "<BR>View the <A HREF = \"README.html\">ReadMe</A> file.\n"
+          "<BR>View the <A HREF = \"README.html\">README</A> file.\n"
         else if file_exists (tack_on (!index_path) "README") then
-          "<BR>View the <A HREF = \"README\">ReadMe</A> file.\n"
+          "<BR>View the <A HREF = \"README\">README</A> file.\n"
         else "") ^
        "<HR>" ^ implode (map main_entry theories) ^ "<!-->");
      TextIO.closeOut out;