changeset 69538 | faf547d2834c |
parent 69536 | 892b68f932f9 |
child 69562 | 636b3c03a61a |
--- a/src/Pure/PIDE/headless.scala Sat Dec 29 16:13:05 2018 +0100 +++ b/src/Pure/PIDE/headless.scala Sat Dec 29 17:37:02 2018 +0100 @@ -433,12 +433,13 @@ { resources => + def options: Options = session_base_info.options + /* session */ def start_session(print_mode: List[String] = Nil, progress: Progress = No_Progress): Session = { - val options = session_base_info.options val session = new Session(session_base_info.session, options, resources) val session_error = Future.promise[String]