# HG changeset patch # User wenzelm # Date 1495882677 -7200 # Node ID 35652d0834f49b4c2cf373989ca68a273bcab2e8 # Parent 79e4d94aa9ad3e18e0334d5a871a669adac6f4c9 tuned signature; diff -r 79e4d94aa9ad -r 35652d0834f4 etc/isabelle.css --- a/etc/isabelle.css Sat May 27 12:52:36 2017 +0200 +++ b/etc/isabelle.css Sat May 27 12:57:57 2017 +0200 @@ -119,3 +119,5 @@ position: absolute; z-index: 1; } + +.tooltip pre { margin: 1px; white-space: pre-wrap; } diff -r 79e4d94aa9ad -r 35652d0834f4 src/Pure/Admin/build_status.scala --- a/src/Pure/Admin/build_status.scala Sat May 27 12:52:36 2017 +0200 +++ b/src/Pure/Admin/build_status.scala Sat May 27 12:57:57 2017 +0200 @@ -259,8 +259,7 @@ if (x == 0L) None else Some(x.toString + " M") HTML.write_document(target_dir, "index.html", - List(HTML.title("Isabelle build status"), - HTML.style("pre { margin: 1px; white-space: pre-wrap; }")), + List(HTML.title("Isabelle build status")), List(HTML.chapter("Isabelle build status"), HTML.par( List(HTML.description(