# HG changeset patch
# User wenzelm
# Date 1649511327 -7200
# Node ID 96293bd077bb6570832993e60980cddb8287e702
# Parent  7b417c578b19dd338565d539bc1a9179be7dbb58
tuned;

diff -r 7b417c578b19 -r 96293bd077bb src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sat Apr 09 15:33:38 2022 +0200
+++ b/src/Pure/Tools/build_job.scala	Sat Apr 09 15:35:27 2022 +0200
@@ -463,10 +463,10 @@
 
       val result = {
         val theory_timing =
-          theory_timings.iterator.map(
+          theory_timings.iterator.flatMap(
             {
-              case props @ Markup.Name(name) => name -> props
-              case _ => ???
+              case props @ Markup.Name(name) => Some(name -> props)
+              case _ => None
             }).toMap
         val used_theory_timings =
           for { (name, _) <- deps(session_name).used_theories }