src/Pure/Thy/export.scala
changeset 75791 fb12433208aa
parent 75790 0ab8a9177e41
child 75824 a2b2e8964e1a
--- a/src/Pure/Thy/export.scala	Sun Aug 07 12:58:59 2022 +0200
+++ b/src/Pure/Thy/export.scala	Sun Aug 07 13:44:01 2022 +0200
@@ -307,7 +307,7 @@
             attempts.collectFirst({ case (name, None) => name }) match {
               case Some(bad) =>
                 for ((_, Some(db)) <- attempts) db.close()
-                store.bad_database(bad)
+                store.error_database(bad)
               case None =>
                 for ((name, Some(db)) <- attempts) yield {
                   new Session_Database(name, db) { override def close(): Unit = this.db.close() }