diff options
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore index 92e9fd2105..bdd692420f 100644 --- a/.gitignore +++ b/.gitignore @@ -113,7 +113,6 @@ doc/stdlib/FullLibrary.coqdoc.tex doc/stdlib/html/ doc/stdlib/index-body.html doc/stdlib/index-list.html -doc/tools/docgram/productionlistGrammar doc/tools/docgram/editedGrammar doc/tools/docgram/prodnGrammar doc/unreleased.rst |