# HG changeset patch # User wenzelm # Date 1514460417 -3600 # Node ID 417e081322ae751037701bf8b16148e6935e5276 # Parent e67abae0e1ca3fcb3b464bcbb3448cefab80023e avoid clash with special files in HTML output; diff -r e67abae0e1ca -r 417e081322ae src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Thu Dec 28 12:20:52 2017 +0100 +++ b/src/Pure/Thy/sessions.scala Thu Dec 28 12:26:57 2017 +0100 @@ -29,7 +29,8 @@ def exclude_session(name: String): Boolean = name == "" || name == DRAFT - def exclude_theory(name: String): Boolean = name == root_name + def exclude_theory(name: String): Boolean = + name == root_name || name == "README" || name == "index" /* base info and source dependencies */