# HG changeset patch
# User wenzelm
# Date 1496919710 -7200
# Node ID 36bf57d6c0116b234698ab3e09829363cfdc1835
# Parent  58d2e41afbfe5b00a51e6ef2caad35583c0801dd
tuned layout (amending 8040d2563593);

diff -r 58d2e41afbfe -r 36bf57d6c011 src/Pure/Thy/present.scala
--- 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)