diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-08-16 09:37:21 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-16 09:37:21 +0200 |
| commit | f052c7fea6b0b9c0628ad77908ede7aac8712bd5 (patch) | |
| tree | 98eed89cf4d4b78806e774716da53ebc1dbbb237 /plugins | |
| parent | f0b4757d291ce3e07c8ccfcd4217d204fd2059ba (diff) | |
| parent | f3bb625fb2d118168042b97162e1ece1bda4a039 (diff) | |
Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords wrongly tagged as keywords
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions