Re: [PATCH] Makefile: mrproper shall delete doc/output/