# HG changeset patch
# User wenzelm
# Date 1494968232 -7200
# Node ID ad35427dbe88ff4dfcf864809e0910bb35ae4713
# Parent  aa6e58dc54d02937f785981ccdc292d96c22d659
less restrictive filter: omit empty charts, but show latest timing;

diff -r aa6e58dc54d0 -r ad35427dbe88 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Tue May 16 16:28:13 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Tue May 16 22:57:12 2017 +0200
@@ -180,8 +180,7 @@
     val sorted_entries =
       (for {
         (name, sessions) <- data_entries.toList
-        sorted_sessions <-
-          proper_list(sessions.toList.map(_._2).filter(_.check_timing).sortBy(_.order))
+        sorted_sessions <- proper_list(sessions.toList.map(_._2).sortBy(_.order))
       }
       yield {
         val hosts = get_hosts(name).toList.sorted
@@ -297,9 +296,11 @@
                   """ using 1:6 smooth csplines title "heap" """)
 
               val plot_names =
-                List(
-                  gnuplot(timing_plots, "timing", timing_range),
-                  gnuplot(ml_timing_plots, "ml_timing", timing_range)) :::
+                (if (session.check_timing)
+                  List(
+                    gnuplot(timing_plots, "timing", timing_range),
+                    gnuplot(ml_timing_plots, "ml_timing", timing_range))
+                 else Nil) :::
                 (if (session.check_heap) List(gnuplot(heap_plots, "heap", "[0:]")) else Nil)
 
               session.name -> plot_names