equal
deleted
inserted
replaced
31 val session_base: Sessions.Base, |
31 val session_base: Sessions.Base, |
32 val log: Logger = No_Logger, |
32 val log: Logger = No_Logger, |
33 command_timings: List[Properties.T] = Nil |
33 command_timings: List[Properties.T] = Nil |
34 ) { |
34 ) { |
35 resources => |
35 resources => |
|
36 |
|
37 |
|
38 override def toString: String = "Resources(" + session_base.toString + ")" |
36 |
39 |
37 |
40 |
38 /* init session */ |
41 /* init session */ |
39 |
42 |
40 def init_session_yxml: String = { |
43 def init_session_yxml: String = { |