diff options
| author | Gaëtan Gilbert | 2018-04-24 16:21:33 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-05-11 13:46:50 +0200 |
| commit | 13139e0353d702392cf2d6987abfc226bc4214b2 (patch) | |
| tree | 31860d96f75f82e552a175ccc7bc0da6b0a63b91 /dev/include | |
| parent | 5c34cfa54ec1959758baa3dd283e2e30853380db (diff) | |
coqdev.el: add bug-reference-mode variables
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions