# HG changeset patch
# User clasohm
# Date 816438501 -3600
# Node ID a60d1abb06c0a865ebfb3aaec6e9c18e90af59c7
# Parent 70ee8d7b22330d42ff1d521fa9f8229913316b0a
added link to README.html or README
diff -r 70ee8d7b2233 -r a60d1abb06c0 src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML Wed Nov 15 13:27:57 1995 +0100
+++ b/src/Pure/Thy/thy_read.ML Wed Nov 15 13:28:21 1995 +0100
@@ -1067,7 +1067,7 @@
val subdir = relative_path base_path (!index_path);
in output (out,
"Isabelle/" ^ subdir ^ "\n\
- \Isabelle/" ^ subdir ^ "
\n\
+ \Isabelle/" ^ subdir ^ "
\n\
\The name of every theory is linked to its theory file
\n\
\![\\/](\"")
stands for subtheories (child theories)
\n\
@@ -1075,8 +1075,13 @@
\\" ALT = /\\> stands for supertheories (parent theories)\n\
\\
- \Back to the index of Isabelle logics.\n
" ^
- main_entries theories (space_explode "/" base_path) ^
+ \Back to the index of Isabelle logics.\n" ^
+ (if file_exists "README.html" then
+ "
View the ReadMe file.\n"
+ else if file_exists "README" then
+ "
View the ReadMe file.\n"
+ else "") ^
+ "
" ^ main_entries theories (space_explode "/" base_path) ^
"\n");
close_out out
end;