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