author | wenzelm |
Thu, 08 Jun 2017 13:01:50 +0200 | |
changeset 66038 | 36bf57d6c011 |
parent 66037 | 58d2e41afbfe |
child 66039 | a2b8c3d31037 |
--- a/src/Pure/Thy/present.scala Thu Jun 08 12:54:55 2017 +0200 +++ b/src/Pure/Thy/present.scala Thu Jun 08 13:01:50 2017 +0200 @@ -57,7 +57,7 @@ sessions.map({ case (name, description) => (List(HTML.link(name + "/index.html", HTML.text(name))), if (description == "") Nil - else List(HTML.pre(HTML.text(description)))) }))))))) + else HTML.break ::: List(HTML.pre(HTML.text(description)))) }))))))) } def make_global_index(browser_info: Path)