This PR/issue depends on:

• [Merged by Bors] - feat: syntax linter for #-commands #11019
  By Dependent Issues (🤖). Happy coding!

This looks good to me, of course!

If you merge master, the diff will become much smaller, now that the linter is in mathlib!

I rebased master (and fixed a typo in the HashCommandLinter's docstring - which I remembered too late).

Thanks for fixing the typo!

I am happy with removing the CI step, although I wonder whether waiting for a couple of days to see them both working at the same time is a good idea.

I'm also happy to wait for a few days - to me, it's just unclear if we would ever get such a signal (since the linter errors locally already).

I think that this is indeed an improvement.

maintainer merge

🚀 Pull request has been placed on the maintainer queue by adomani.

Thanks 🎉

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style