# HG changeset patch
# User wenzelm
# Date 1680094795 -7200
# Node ID 4855150bc98bbd489a7a2fe67093b0c36cb993bc
# Parent  ebf70b199db7022fca05202e9f19b75881d10907
tuned output;

diff -r ebf70b199db7 -r 4855150bc98b src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Wed Mar 29 14:52:54 2023 +0200
+++ b/src/Pure/Admin/build_log.scala	Wed Mar 29 14:59:55 2023 +0200
@@ -815,6 +815,18 @@
     new Store(options, cache)
 
   class Store private[Build_Log](options: Options, val cache: XML.Cache) {
+    override def toString: String = {
+      val s =
+        Exn.capture { open_database() } match {
+          case Exn.Res(db) =>
+            val db_name = db.toString
+            db.close()
+            "database = " + db_name
+          case Exn.Exn(_) => "no database"
+        }
+      "Store(" + s + ")"
+    }
+
     def open_database(
       user: String = options.string("build_log_database_user"),
       password: String = options.string("build_log_database_password"),