[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PATCH 1/5] maint: add entries to 'doc/.gitignore'
From: |
Bernhard Voelker |
Subject: |
[PATCH 1/5] maint: add entries to 'doc/.gitignore' |
Date: |
Wed, 1 Jan 2020 21:50:52 +0100 |
* doc/.gitignore (/find.html/, /find-maint.html/): Add entries for
HTML output directories.
(/find.pdf, /find-maint.pdf): Add entries for PDF files.
(/find-maint.dvi, /find-maint.ps): Add entries for other formats.
---
doc/.gitignore | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/doc/.gitignore b/doc/.gitignore
index a951f73e..af391e36 100644
--- a/doc/.gitignore
+++ b/doc/.gitignore
@@ -7,16 +7,22 @@
/find.dvi
/find.fn
/find.fns
+/find.html/
/find.info
/find.info-1
/find.info-2
/find.ky
/find.log
+/find.pdf
/find.pg
/find.ps
/find.toc
/find.tp
/find.vr
+/find-maint.dvi
+/find-maint.html/
+/find-maint.pdf
+/find-maint.ps
/stamp-vti
/version.texi
/texinfo.tex
--
2.24.1