src/Pure/Thy/sessions.scala
changeset 71599 23d0a45a9283
parent 71595 01d92325ddab
child 71601 97ccf48c2f0c
--- a/src/Pure/Thy/sessions.scala	Fri Mar 27 12:46:56 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Mar 27 13:02:56 2020 +0100
@@ -336,7 +336,6 @@
   /* base info */
 
   sealed case class Base_Info(
-    options: Options,
     session: String,
     sessions_structure: Structure,
     errors: List[String],
@@ -419,7 +418,7 @@
 
     val deps1 = Sessions.deps(selected_sessions1, progress = progress)
 
-    Base_Info(options, session1, full_sessions1, deps1.errors, deps1(session1), infos1)
+    Base_Info(session1, full_sessions1, deps1.errors, deps1(session1), infos1)
   }