It's a lot nicer than manually maintaining .gitignore in general. Closes: #235 Approved by: giuseppe
This is preparation for introducing a `mkdocs` manual under `doc/` which should be significantly more useful for the world at large than the minimal manual that exists there now.