Or, if we don't want auto-commits that aren't attached to any user account, we could fail the PR instead if we detect any changes after running make all
TODO
[ ] Decide on whether auto-commit should be a thing
[ ] If so, what should its name/email be?
[ ] Set a proper maintainer (it probably shouldn't be me)
GitHub Actions help automate workflows.
One cumbersome workflow we have is that all our Markdown files are converted to HTML, formatters are run, files are highlighted...
So, this new "publish" action runs on every push to master and calls
make all
, followed by a push back to master with any changed files.This actually enables some cool things we could do:
make all
TODO