diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-10 20:46:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-10 20:46:19 +0200 |
| commit | 5da17b8c60846913db18b0f9216d63898933aa52 (patch) | |
| tree | 365f4b54a645e23f9f702eb7e343182dcac34179 /test-suite/misc | |
| parent | e559f7553030dc3a86936794d0f80f39b0131960 (diff) | |
| parent | 818ba539cf4a0aed2172f370dcddd380b6ec6a4c (diff) | |
Merge PR #7437: [coqdep] Minor cleanups.
Diffstat (limited to 'test-suite/misc')
0 files changed, 0 insertions, 0 deletions