From 085d01942d5bfea2461b9fab95438a4c2ed1b56d Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 21 Mar 2024 18:43:29 +0100
Subject: [PATCH] fix: restore default of `stderrAsMessages` (#3733)

Puts trace.compiler back in the info view. Apparently an unintended
change in #3014.
---
 src/Lean/Language/Lean.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean
index 82fa7349a8..c967565bf3 100644
--- a/src/Lean/Language/Lean.lean
+++ b/src/Lean/Language/Lean.lean
@@ -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"
 }