Fix problems with building PDF documentation

The PDF documents were sometimes generated without their tables of contents.
This could happen if for some reason there was no .toc file but the .dvi
file still existed.  The Mmakefile would not run texi2dvi which would
normally produce a toc file if the .dvi file already existed, this caused
pdftex to fail to include the table of contents in the generated PDF file.

This was common as distclean deleted the .toc file but did not delete the
.dvi file, so this commonly happened when generating documentation from a
source distribution tarball as we do for the webpage.

This change causes distclean to also delete the .dvi files.

doc/Mmakefile:
    As above

    Also make library.dvi depend upon library-menu.texi_pp
    and library-chapters.texi_pp
Merge branch 'version-13_05-branch'
Update .gitignore files

doc/.gitignore:
    .gitignore several generated file extensions.

runtime/.gitignore:
    .gitignore the tags file.