src/Pure/Thy/sessions.scala
changeset 66976 806bc39550a5
parent 66975 ca73d44d51aa
child 66977 fa79f18eadc7
--- a/src/Pure/Thy/sessions.scala	Wed Nov 01 16:38:15 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Nov 01 16:43:51 2017 +0100
@@ -335,9 +335,7 @@
     def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors))
   }
 
-  def session_base_info(
-    options: Options,
-    session: String,
+  def base_info(options: Options, session: String,
     dirs: List[Path] = Nil,
     all_known: Boolean = false,
     required_session: Boolean = false): Base_Info =