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() }