From fa35dd6e40d2f5089b3d0a18cb6337ade4eae760 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 10 Oct 2018 19:32:45 +0200
Subject: [doc] [sphinx] Fix title levels.

---
 .gitignore | 1 -
 1 file changed, 1 deletion(-)

(limited to '.gitignore')

diff --git a/.gitignore b/.gitignore
index 39ef20970d..05869e2a0c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -101,7 +101,6 @@ doc/faq/axioms.pdf_t
 doc/faq/axioms.png
 doc/sphinx/index.rst
 doc/sphinx/zebibliography.rst
-doc/sphinx/credits.rst
 doc/stdlib/Library.out
 doc/stdlib/Library.ps
 doc/stdlib/Library.coqdoc.tex
-- 
cgit v1.2.3