diff options
| author |  Stephane Glondu <steph@glondu.net> | 2017-09-26 11:07:18 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2017-09-26 11:09:14 +0200 |
| commit | 090592236763255a379552fca40bb865b68c73e6 (patch) | |
| tree | e849e2b822262ec8af1c9f8569afcbb60d0de4de /debian/coqide.menu | |
| parent | c2f1eda504659079238313826fc9c60e981af531 (diff) | |
Remove unused Lintian overrides
Diffstat (limited to 'debian/coqide.menu')
0 files changed, 0 insertions, 0 deletions