Subject: Re: bug#36014: [PATCH] Attempt to use console-fonts not provided by kbd if they are installed
From: Ludovic Courtès <[email-masked]>
To: John Soo <[email-masked]>
Cc: [email-masked]
Date: Thu, 22 Aug 2019 18:00:00 +0200
List-Id: <debbugs-submit.debbugs.gnu.org>

Hello,

John Soo <[email-masked]> skribis:

> I am not familiar with the info and html documentation build process. Will
> this patch suffice?

Sure; I pushed a slightly modified variant as commit
74a98b5cddd0430dd7229d4045f4885191c624b7.

Thanks,
Ludo’.