diff options
| author | Gaëtan Gilbert | 2020-02-20 13:59:44 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-20 13:59:44 +0100 |
| commit | 01f8d7666b282b0913ddc266d842d986e12976fa (patch) | |
| tree | 6869b2e3400924076fed1d60e95fea57c96308c2 | |
| parent | aee284e64c97dce0112e36a7f225d14391533f11 (diff) | |
| parent | 22c09533551f65ffa4472371711eb368163a55b2 (diff) | |
Merge PR #11633: Add doc/unreleased.rst to .gitignore.
Reviewed-by: SkySkimmer
| -rw-r--r-- | .gitignore | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/.gitignore b/.gitignore index 489e6211a7..b665b2f86d 100644 --- a/.gitignore +++ b/.gitignore @@ -115,9 +115,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 |