# HG changeset patch
# User wenzelm
# Date 1494322158 -7200
# Node ID 84a0ac8a046ef1ba6c7e870dc1cf7621685d2e3d
# Parent  6107504371fb26052ffaab5645e3f3824e7dc7d4
tuned;

diff -r 6107504371fb -r 84a0ac8a046e src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Tue May 09 11:21:42 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Tue May 09 11:29:18 2017 +0200
@@ -165,10 +165,18 @@
     target_dir: Path = default_target_dir,
     image_size: (Int, Int) = default_image_size)
   {
+    Isabelle_System.mkdirs(target_dir)
+    File.write(target_dir + Path.basic("index.html"),
+      HTML.output_document(
+        List(HTML.title("Isabelle build status")),
+        List(HTML.chapter("Isabelle build status (" + data.date + ")"),
+          HTML.itemize(data.entries.map({ case (data_name, _) =>
+            List(HTML.link(clean_name(data_name) + "/index.html", HTML.text(data_name))) })))))
+
     for ((data_name, sessions) <- data.entries) {
+      progress.echo("output " + quote(data_name))
+
       val dir = target_dir + Path.basic(clean_name(data_name))
-
-      progress.echo("output " + quote(data_name))
       Isabelle_System.mkdirs(dir)
 
       val session_plots =
@@ -273,13 +281,6 @@
                     HTML.width(image_size._1 / 2) +
                     HTML.height(image_size._2 / 2)))))))
     }
-
-    File.write(target_dir + Path.basic("index.html"),
-      HTML.output_document(
-        List(HTML.title("Isabelle build status")),
-        List(HTML.chapter("Isabelle build status (" + data.date + ")"),
-          HTML.itemize(data.entries.map({ case (data_name, _) =>
-            List(HTML.link(clean_name(data_name) + "/index.html", HTML.text(data_name))) })))))
   }