# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1493732057 -3600
# Node ID eba08da54c6b59e995c16609b1fccd0e10f4b846
# Parent  45632d594bdb912e02ee62250a58025b3ef6f396# Parent  378a2f11bec97318dce834933fdf4e4b4c8408c0
Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.VldMQI

diff -r 378a2f11bec9 -r eba08da54c6b src/HOL/ROOT
--- a/src/HOL/ROOT	Tue May 02 14:34:06 2017 +0100
+++ b/src/HOL/ROOT	Tue May 02 14:34:17 2017 +0100
@@ -71,7 +71,7 @@
     Approximations
     Circle_Area
 
-session "HOL-Computational_Algebra" in "Computational_Algebra" = "HOL-Library" +
+session "HOL-Computational_Algebra" (timing) in "Computational_Algebra" = "HOL-Library" +
   theories
     Computational_Algebra
     (*conflicting type class instantiations and dependent applications*)
@@ -562,7 +562,7 @@
   theories CompleteLattice
   document_files "root.tex"
 
-session "HOL-ex" in ex = "HOL-Library" +
+session "HOL-ex" (timing) in ex = "HOL-Library" +
   description {*
     Miscellaneous examples for Higher-Order Logic.
   *}
diff -r 378a2f11bec9 -r eba08da54c6b src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Tue May 02 14:34:06 2017 +0100
+++ b/src/Pure/Admin/build_log.scala	Tue May 02 14:34:17 2017 +0100
@@ -533,7 +533,7 @@
     val Session_Finished2 =
       new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
     val Session_Timing =
-      new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
+      new Regex("""^Timing (\S+) \((\d+) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
     val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
     val Session_Failed = new Regex("""^(\S+) FAILED""")
     val Session_Cancelled = new Regex("""^(\S+) CANCELLED""")