fix: restore default of stderrAsMessages (#3733)
Puts trace.compiler back in the info view. Apparently an unintended change in #3014.
This commit is contained in:
parent
31767aa835
commit
085d01942d
1 changed files with 1 additions and 1 deletions
|
|
@ -71,7 +71,7 @@ private def pushOpt (a? : Option α) (as : Array α) : Array α :=
|
|||
|
||||
/-- Option for capturing output to stderr during elaboration. -/
|
||||
register_builtin_option stderrAsMessages : Bool := {
|
||||
defValue := false
|
||||
defValue := true
|
||||
group := "server"
|
||||
descr := "(server) capture output to the Lean stderr channel (such as from `dbg_trace`) during elaboration of a command as a diagnostic message"
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue