From 906b88c665d12f31aa9cd584fc2c7c66edef434f Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 12 Apr 2021 16:38:24 +0200
Subject: Gitignore update for doc_grammar.

---
 .gitignore | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.gitignore b/.gitignore
index bf7430cc2e..1abead3c67 100644
--- a/.gitignore
+++ b/.gitignore
@@ -115,6 +115,9 @@ doc/stdlib/index-body.html
 doc/stdlib/index-list.html
 doc/tools/docgram/editedGrammar
 doc/tools/docgram/prodnGrammar
+doc/tools/docgram/prodnCommands
+doc/tools/docgram/prodnTactics
+doc/tools/docgram/updated_rsts
 doc/unreleased.rst
 
 # .mll files
-- 
cgit v1.2.3