src/Pure/Tools/profiling_report.scala
changeset 75791 fb12433208aa
parent 75780 f49c4f160b84
child 76205 005abcb34849
--- a/src/Pure/Tools/profiling_report.scala	Sun Aug 07 12:58:59 2022 +0200
+++ b/src/Pure/Tools/profiling_report.scala	Sun Aug 07 13:44:01 2022 +0200
@@ -19,7 +19,7 @@
 
     using(Export.open_session_context0(store, session)) { session_context =>
       session_context.session_db().map(db => store.read_theories(db, session)) match {
-        case None => error("Missing build database for session " + quote(session))
+        case None => store.error_database(session)
         case Some(used_theories) =>
           theories.filterNot(used_theories.toSet) match {
             case Nil =>