diff options
| author | Pierre-Marie Pédrot | 2018-05-07 11:31:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-05-07 11:31:24 +0200 |
| commit | 401e278be6e1f95d1175c5bcb1e33674074988dd (patch) | |
| tree | 70478ca423ebda61fcd23006f88025a8ebba37dc /dev/tools/pre-commit | |
| parent | cee82a36b21c7a87fe4f626d8d72fd938a825648 (diff) | |
| parent | cb37784d2ad3f641af6d3555c0f62050f6543d0d (diff) | |
Merge PR #7427: Fix #7413: coqdep warning on repeated files
Diffstat (limited to 'dev/tools/pre-commit')
0 files changed, 0 insertions, 0 deletions