diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-09-24 08:23:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-09-24 08:26:24 +0200 |
| commit | 8a031dc29abf1e16b2ee78322a7221b8b5c19a33 (patch) | |
| tree | 8095b021d3ed73ee9162529a6a3ff4fcbd209a9e /config | |
| parent | f2f146a997e92f3380d9cd9aa0f7aef80f50dba8 (diff) | |
Fixing unsetting of CoqIDE tags.
Diffstat (limited to 'config')
0 files changed, 0 insertions, 0 deletions