equal
deleted
inserted
replaced
131 -- "build process output tail shown to user (in lines, 0 = unlimited)" |
131 -- "build process output tail shown to user (in lines, 0 = unlimited)" |
132 |
132 |
133 option profiling : string = "" |
133 option profiling : string = "" |
134 -- "ML profiling (possible values: time, allocations)" |
134 -- "ML profiling (possible values: time, allocations)" |
135 |
135 |
|
136 option system_log : string = "" |
|
137 -- "output for system messages (log file or \"-\" for console progress)" |
|
138 |
136 option system_heaps : bool = false |
139 option system_heaps : bool = false |
137 -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS" |
140 -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS" |
138 |
141 |
139 |
142 |
140 section "ML System" |
143 section "ML System" |