From 22c09533551f65ffa4472371711eb368163a55b2 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 19 Feb 2020 18:33:04 +0100
Subject: Add doc/unreleased.rst to .gitignore.

And remove outdated entries on tutorials.
---
 .gitignore | 4 +---
 1 file changed, 1 insertion(+), 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
 
-- 
cgit v1.2.3