diff options
| author | Maxime Dénès | 2017-12-27 10:19:40 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-27 10:19:40 +0100 |
| commit | 37b198dc2ddf2f22e548a60a163607cfc6fbf4b5 (patch) | |
| tree | cdad1cb00a55d5ce4e0e36d851bad1c3326e04a8 /dev/tools/github-check-prs.py | |
| parent | f6857ce53ecf64b0086854495b4a8451f476d5b4 (diff) | |
| parent | b455e96cce263ea48ff0aa8b8ebf530d0f1eea9c (diff) | |
Merge PR #6040: Making coq_makefile usage consistent with what it claims + possibly fixing printing errors (was: Removing failure of coq_makefile on no arguments)
Diffstat (limited to 'dev/tools/github-check-prs.py')
0 files changed, 0 insertions, 0 deletions