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 /.gitignore | |
| 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 '.gitignore')
| -rw-r--r-- | .gitignore | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore index 71de7bb8d..5ee2f3f77 100644 --- a/.gitignore +++ b/.gitignore @@ -84,6 +84,8 @@ test-suite/coq-makefile/*/subdir/done test-suite/coq-makefile/merlin1/.merlin test-suite/coq-makefile/plugin-reach-outside-API-and-fail/_CoqProject test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/_CoqProject +test-suite/coqdoc/Coqdoc.* +test-suite/coqdoc/index.html # documentation |