diff options
Diffstat (limited to 'manual')
-rw-r--r-- | manual/.gitignore | 37 |
1 files changed, 17 insertions, 20 deletions
diff --git a/manual/.gitignore b/manual/.gitignore index 27f045cc1f..e92cef39b4 100644 --- a/manual/.gitignore +++ b/manual/.gitignore @@ -1,32 +1,29 @@ -*.dvi* -*.info* -*.c.texi -*.ps -*.pdf -*.toc *.aux -*.log -*.tmp +*.c.texi *.cp *.cps +*.dvi* *.fn *.fns -*.vr -*.vrs -*.tp -*.tps +*.info* *.ky *.kys +*.log +*.pdf *.pg *.pgs - -texis -top-menu.texi +*.ps +*.tmp +*.toc +*.tp +*.tps +*.vr +*.vrs chapters.texi -summary.texi -stamp-* -distinfo -dir-add.texinfo dir-add.texi - +dir-add.texinfo libm-err.texi +stamp-* +summary.texi +texis +top-menu.texi |