diff options
| author | Théo Zimmermann | 2020-09-11 12:39:39 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-09-11 12:39:39 +0200 |
| commit | 795af932ef6606ba8385448244f60c728e9abdbd (patch) | |
| tree | ccbe1956742176260fcb9b5ff5814570bf216bfa /.gitignore | |
| parent | 6abc0f4de27e4c0ecbbc7736388682abe21ebd7f (diff) | |
Remove outdated references to productionlist.
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 |