src/Pure/ML/ml_process.scala
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 =
   {