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