diff options
| author | Gaëtan Gilbert | 2019-03-29 00:14:58 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-29 00:14:58 +0100 |
| commit | 4b9636ffd47ea5a0b99df442047ba03d18422738 (patch) | |
| tree | 592bec96faac3cc2e5f203f4e374d41353d23457 /dev/include | |
| parent | 688e20c432d2639050a62703e1c566ddfbe42b2a (diff) | |
| parent | 8ad84a3541bee26d1ba0644274dcf4d9e287c124 (diff) | |
Merge PR #9834: Ignore generated files for CoqIDE bindings
Reviewed-by: gares
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions