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