diff options
| author | Pierre-Marie Pédrot | 2018-07-23 14:40:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-23 14:40:49 +0200 |
| commit | f37c6f514a63aa1ebfb23b3c8def0087c242ca15 (patch) | |
| tree | 604e0a0b648787889b8585465d5e433b3c7504fb /dev/include | |
| parent | 1bfe8872b07ca4ee05c1c60ace506d87cda9d41c (diff) | |
Fix deprecated warnings from Pcoq.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions