equal
deleted
inserted
replaced
14 session_name: String, |
14 session_name: String, |
15 val info: Sessions.Info, |
15 val info: Sessions.Info, |
16 deps: Sessions.Deps, |
16 deps: Sessions.Deps, |
17 store: Sessions.Store, |
17 store: Sessions.Store, |
18 do_store: Boolean, |
18 do_store: Boolean, |
19 presentation: Presentation.Context, |
|
20 verbose: Boolean, |
19 verbose: Boolean, |
21 val numa_node: Option[Int], |
20 val numa_node: Option[Int], |
22 command_timings0: List[Properties.T]) |
21 command_timings0: List[Properties.T]) |
23 { |
22 { |
24 val options: Options = NUMA.policy_options(info.options, numa_node) |
23 val options: Options = NUMA.policy_options(info.options, numa_node) |