Documentation / .gitignoreon commit Merge branch 'jc/push' (5bcbc7f)
   1*.xml
   2*.html
   3*.1
   4*.7
   5*.made
   6howto-index.txt
   7doc.dep
   8cmds-*.txt