diff options
| author | Théo Zimmermann | 2020-02-19 18:33:04 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-02-19 18:33:04 +0100 |
| commit | 22c09533551f65ffa4472371711eb368163a55b2 (patch) | |
| tree | c644ff2576d0e762386f0fabac54e435a021682f /.gitignore | |
| parent | 43c3c7d6f62a9bee4772242c27fbafd54770d271 (diff) | |
Add doc/unreleased.rst to .gitignore.
And remove outdated entries on tutorials.
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/.gitignore b/.gitignore index b99d2a0d45..760ccc60c3 100644 --- a/.gitignore +++ b/.gitignore @@ -118,9 +118,7 @@ doc/stdlib/index-list.html doc/tools/docgram/productionlistGrammar doc/tools/docgram/editedGrammar doc/tools/docgram/prodnGrammar -doc/tutorial/Tutorial.v.out -doc/RecTutorial/RecTutorial.html -doc/RecTutorial/RecTutorial.ps +doc/unreleased.rst # .mll files |