equal
deleted
inserted
replaced
260 |
260 |
261 def print_heap(x: Long): Option[String] = |
261 def print_heap(x: Long): Option[String] = |
262 if (x == 0L) None else Some(x.toString + " M") |
262 if (x == 0L) None else Some(x.toString + " M") |
263 |
263 |
264 HTML.write_document(target_dir, "index.html", |
264 HTML.write_document(target_dir, "index.html", |
265 List(HTML.title("Isabelle build status")), |
265 List(HTML.title("Isabelle build status"), |
|
266 HTML.style("pre { margin: 1px; white-space: pre-wrap; }")), |
266 List(HTML.chapter("Isabelle build status"), |
267 List(HTML.chapter("Isabelle build status"), |
267 HTML.par( |
268 HTML.par( |
268 List(HTML.description( |
269 List(HTML.description( |
269 List(HTML.text("status date:") -> HTML.text(data.date.toString))))), |
270 List(HTML.text("status date:") -> HTML.text(data.date.toString))))), |
270 HTML.par( |
271 HTML.par( |