changeset 75916 | b6589c8ccadd |
parent 75906 | 2167b9e3157a |
child 75917 | 20b918404aa3 |
--- a/src/Pure/Thy/sessions.scala Fri Aug 19 21:43:06 2022 +0200 +++ b/src/Pure/Thy/sessions.scala Fri Aug 19 23:58:44 2022 +0200 @@ -34,7 +34,7 @@ def exclude_session(name: String): Boolean = name == "" || name == DRAFT def exclude_theory(name: String): Boolean = - name == root_name || name == "README" || name == "index" || name == "bib" + name == root_name || name == "index" || name == "bib" /* ROOTS file format */