equal
deleted
inserted
replaced
139 port: Int = 0, |
139 port: Int = 0, |
140 historic: Boolean = false, |
140 historic: Boolean = false, |
141 history: Int = 0, |
141 history: Int = 0, |
142 history_base: String = "build_history_base", |
142 history_base: String = "build_history_base", |
143 components_base: String = Components.dynamic_components_base, |
143 components_base: String = Components.dynamic_components_base, |
144 clean_components: Boolean = false, |
144 clean_components: Boolean = true, |
145 java_heap: String = "", |
145 java_heap: String = "", |
146 options: String = "", |
146 options: String = "", |
147 args: String = "", |
147 args: String = "", |
148 afp: Boolean = false, |
148 afp: Boolean = false, |
149 bulky: Boolean = false, |
149 bulky: Boolean = false, |