diff options
| author | Théo Zimmermann | 2018-10-10 19:32:45 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-10-10 19:34:06 +0200 |
| commit | fa35dd6e40d2f5089b3d0a18cb6337ade4eae760 (patch) | |
| tree | 9c0cb4d41681f04bc9a2c5527928df67002244a9 /.gitignore | |
| parent | 7489829eff2b36b15694a7f06122fc825905bba6 (diff) | |
[doc] [sphinx] Fix title levels.
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 1 |
1 files changed, 0 insertions, 1 deletions
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 |