diff options
| author | Pierre-Marie Pédrot | 2016-09-27 18:28:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-27 18:28:48 +0200 |
| commit | 72c1fefcfb3f0dff02005034685f6b58ff84b3cc (patch) | |
| tree | b3618351d80a7519d75c65d198445be572ae0391 /dev/tools | |
| parent | e8b9ee76af721c32b2d5cfcdae4ecbf47b341545 (diff) | |
Fix bug #4553: CoqIDE gives warnings about deprecated GTK features.
Diffstat (limited to 'dev/tools')
0 files changed, 0 insertions, 0 deletions