mirror of
https://github.com/jgm/pandoc.git
synced 2026-08-28 17:20:47 +08:00
f01b2dfe28
This is useless because it runs after the push; we need this check for pull requests but not for core committers. (They should use a pre-commit hook.)