diff options
| author | Hugo Herbelin | 2017-11-04 19:46:50 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-12-23 02:35:25 +0100 |
| commit | 143244e0606a790b73da2360fb0eabe3d98d4b4e (patch) | |
| tree | e9bccdb8961ce6444f64fab557397e2a8e3ed093 /dev/tools/github-check-prs.py | |
| parent | d9f79d97dbc503e149cba2df1b228a94d7ac970b (diff) | |
Removing failure of coq_makefile on no arguments.
Nevertheless making option -o of coq_makefile recommended as discussed
in PR#6040.
This is one way to resolve the inconsistency with the usage which says
that all arguments are optional.
Diffstat (limited to 'dev/tools/github-check-prs.py')
0 files changed, 0 insertions, 0 deletions