equal
deleted
inserted
replaced
122 def session_build( |
122 def session_build( |
123 options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int = |
123 options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int = |
124 { |
124 { |
125 val mode = session_build_mode() |
125 val mode = session_build_mode() |
126 |
126 |
127 Build.build(options = session_options(options), progress = progress, |
127 Build.build(session_options(options), progress = progress, build_heap = true, |
128 build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system", |
128 no_build = no_build, system_mode = mode == "" || mode == "system", |
129 dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos, |
129 dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos, |
130 sessions = List(PIDE.resources.session_name)).rc |
130 sessions = List(PIDE.resources.session_name)).rc |
131 } |
131 } |
132 |
132 |
133 def session_start(options: Options) |
133 def session_start(options: Options) |