mirror of
https://github.com/pmret/papermario.git
synced 2024-11-18 08:52:40 +01:00
6cd56e72c1
We now lint ALL files in the repository, not just those detected as changed in the commit (the procedure to do this failed when HEAD was exactly 1 commit ahead of the base branch). Also we now only lint pull requests, not in-progress pushes to any branch. |
||
---|---|---|
.. | ||
coverage.yaml | ||
lint.yaml |