Also:
- clean unused files in pics/
- (re)add some minor german spell checking
- remove PDFs from gitignore, to allow PDF files in pics/

The last item has the consequence that the PDF file of document
generated by pdflatex gets added to the history at each commit,
increasing the size of .git invain. For the moment it's not clear how we
could get rid of this disadvantage.