--- 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; }
--- 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(