redundant;
authorwenzelm
Fri, 05 Aug 2022 16:40:06 +0200
changeset 75765 b10c3d9dd48a
parent 75764 07e097f60b85
child 75766 d795d8b59563
redundant;
src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Aug 05 14:44:47 2022 +0200
+++ b/src/Pure/Thy/export.scala	Fri Aug 05 16:40:06 2022 +0200
@@ -341,8 +341,6 @@
   def open_context(store: Sessions.Store): Context =
     new Context(store.open_database_context()) { override def close(): Unit = db_context.close() }
 
-  def open_context(options: Options): Context = open_context(Sessions.store(options))
-
   class Session_Database private[Export](val session: String, val db: SQL.Database) {
     def close(): Unit = ()
   }