Subject: Re: [bug#72539] [PATCH] doc: Remove duplicate search paths instructions.
From: "pelzflorian (Florian Pelz)" <[email-masked]>
To: [email-masked]
Cc: Ludovic Courtès <[email-masked]>, Maxim Cournoyer <[email-masked]>, Matthew Trzcinski <[email-masked]>
Date: Mon, 26 Aug 2024 19:43:33 +0200
List-Id: <debbugs-submit.debbugs.gnu.org>

Pushed as 4aaa0ea06fdb2bc00e62e80d504e7778bb6d69de.

Regards,
Florian