* .gitignore: Also ignore doc/*/*/*.html and .ps.