equal
deleted
inserted
replaced
102 -- "build process output tail shown to user (in lines, 0 = unlimited)" |
102 -- "build process output tail shown to user (in lines, 0 = unlimited)" |
103 |
103 |
104 |
104 |
105 section "ML System" |
105 section "ML System" |
106 |
106 |
|
107 option ML_print_depth : int = 20 |
|
108 -- "ML print depth for toplevel pretty-printing" |
|
109 |
107 public option ML_exception_trace : bool = false |
110 public option ML_exception_trace : bool = false |
108 -- "ML exception trace for toplevel command execution" |
111 -- "ML exception trace for toplevel command execution" |
109 |
112 |
110 public option ML_exception_debugger : bool = false |
113 public option ML_exception_debugger : bool = false |
111 -- "ML debugger exception trace for toplevel command execution" |
114 -- "ML debugger exception trace for toplevel command execution" |