diff options
| -rw-r--r-- | .gitignore | 16 |
1 files changed, 2 insertions, 14 deletions
@@ -15,17 +15,5 @@ __pycache__/ *.bz2 *.xz *~ -splashtool.aux -splashtool.cp -splashtool.fn -splashtool.ky -splashtool.log -splashtool.pg -splashtool.toc -splashtool.tp -splashtool.vr -splashtool.info -splashtool.ps -splashtool.pdf -splashtool.dvi - +splashtool.* +!splashtool.texinfo |