On Mon, 29 Oct 2018 at 21:37, Bruno Haible <address@hidden> wrote:
[Changed the subject to something meaningful]
Sorry about that; I only noticed after forwarding that I'd forgotten.
Thanks for the change, which sounds good to me unless there's some other GPL-licensed version of make (so it might mention "GNU General Public License" in the output); it might be better explicitly to check the first line of the output?