commit: 04ccf7cb2800b2073dc999ea511d5afc3f77133c

[log]
author: Kim Morrison <kim@tqft.net>

Mon Mar 02 13:46:47 2026 +0000
committer: Kim Morrison <kim@tqft.net>

Mon Mar 02 13:46:47 2026 +0000
tree: a0c9579d217e0d2eae386d1a96d79bef0fd48140
parent: 786584154764dbccec12d16e00cca979e09d726b [diff]

fix: remove expected constructorNameAsVariable warnings from unrelated tests

These tests are not testing the constructorNameAsVariable linter. Now
that the linter correctly respects `linter.all`, the test harness's
`-Dlinter.all=false` suppresses these warnings.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

2 files changed

tree: a0c9579d217e0d2eae386d1a96d79bef0fd48140

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.