# HG changeset patch
# User wenzelm
# Date 1495021966 -7200
# Node ID cf24cc0b0a47c5e3be2da4e9dc1099ee47b6c5e8
# Parent  6ba2dc4552cace4fbddd5e99858a1f6014fa0ffc
tuned;

diff -r 6ba2dc4552ca -r cf24cc0b0a47 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Wed May 17 13:50:30 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Wed May 17 13:52:46 2017 +0200
@@ -467,7 +467,6 @@
     status: Option[Session_Status.Value] = None,
     ml_statistics: List[Properties.T] = Nil)
   {
-    def proper_chapter: Option[String] = if (chapter == "") None else Some(chapter)
     def proper_groups: Option[String] = if (groups.isEmpty) None else Some(cat_lines(groups))
     def finished: Boolean = status == Some(Session_Status.finished)
   }
@@ -863,7 +862,7 @@
         for ((session_name, session) <- entries_iterator) {
           stmt.string(1) = log_name
           stmt.string(2) = session_name
-          stmt.string(3) = session.proper_chapter
+          stmt.string(3) = proper_string(session.chapter)
           stmt.string(4) = session.proper_groups
           stmt.int(5) = session.threads
           stmt.long(6) = session.timing.elapsed.proper_ms