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 =