diff options
| author | Enrico Tassi | 2019-02-11 17:36:32 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-02-11 17:36:32 +0100 |
| commit | 0a18d769c88372eca162cf7a2f2eec61165c1f77 (patch) | |
| tree | 753aea56358ae638c89470e857244852243d4d0b /Makefile.ci | |
| parent | 22f240bd878647be381e9a60bc4944c3a743acc9 (diff) | |
| parent | 6c29129ee903a0070ae1002089bd2c1ecf0b26c0 (diff) | |
Merge PR #9544: [coqargs] Minor refactoring of error functions.
Reviewed-by: gares
Diffstat (limited to 'Makefile.ci')
0 files changed, 0 insertions, 0 deletions