Zulip Chat Archive
Stream: general
Topic: indentation linter
Johan Commelin (Dec 10 2021 at 08:49):
The indentation linter doesn't seem to be working. E.g.: #9925 has braces with wrong indentation level.
If someone wants to debug this, please go ahead! It will be Xmas before I can look at this.
Last updated: Dec 20 2023 at 11:08 UTC