Re: clean up left over html files

[Alfred M. Szmidt]

GNU makeinfo doesn't know about previously generated files, so it
cannot know what to clean out (maybe the user created them).  If you
wish to do that, use a make target that cleans them out for you.