--- 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"),