Commit 2024-06-17 20:45 13d4164a

View on Github →

fix(test/Lint.lean): re-enable test for duplicate namespaces (#13670) There is a standard hack for dealing with linters running on #guard_msg themselves - so re-enable the test using it. One test broke during the std->batteries rename; fix it.

Estimated changes