changeset 67052 | caf87d4b9b61 |
parent 67026 | 687c822ee5e3 |
child 67219 | 81e9804b2014 |
--- a/src/Pure/ML/ml_process.scala Sat Nov 11 18:41:08 2017 +0000 +++ b/src/Pure/ML/ml_process.scala Sun Nov 12 12:41:05 2017 +0100 @@ -23,7 +23,7 @@ redirect: Boolean = false, cleanup: () => Unit = () => (), channel: Option[System_Channel] = None, - sessions: Option[Sessions.T] = None, + sessions: Option[Sessions.Structure] = None, session_base: Option[Sessions.Base] = None, store: Sessions.Store = Sessions.store()): Bash.Process = {