Re: [PATCH 0/2] Makefile: make coverage optional