diff options
| author | Pierre-Marie Pédrot | 2018-11-17 19:04:24 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-17 19:04:24 +0100 |
| commit | 7d78085e47ec375c23546dfe5df9eb1b4b7d0f39 (patch) | |
| tree | 8722726b471087faf680769123274e4974841fa3 /dev/base_include | |
| parent | 71938f0de10e1f3b69b1158b80b4898bf3a7dfdb (diff) | |
| parent | 4e9bc09df64cd15e85c19ecabbc9580c00771176 (diff) | |
Merge PR #8914: [CoqProject] Abstract warning function for CoqProject readers.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions