commit: 085d01942d5bfea2461b9fab95438a4c2ed1b56d

[log]
author: Sebastian Ullrich <sebasti@nullri.ch>

Thu Mar 21 18:43:29 2024 +0100
committer: GitHub <noreply@github.com>

Thu Mar 21 17:43:29 2024 +0000
tree: 67e025f7a1eb7448a1b770619b55c5c48a8a975e
parent: 31767aa8358ce2b7f4f367a11df7c530e6534236 [diff]

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[diff]

1 file changed

tree: 67e025f7a1eb7448a1b770619b55c5c48a8a975e

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.