Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Tweak the import tree sitter hlgroups.
(This still isn't really used yet until/unless tree-sitter-lean is revived. But the hlgroup is wrong as-is so may as well fix it.)
- Loading branch information