bug#36014: [PATCH] Attempt to use console-fonts not provided by kbd if they are installed

[Ludovic Courtès]

Hello,

John Soo <js...@asu.edu> 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’.