On Tue, Feb 13, 2024 at 07:15:48AM -0500, Greg Wooledge wrote: > This is an obvious bug in the info page. I wonder how many years > this has gone unnoticed. I've filed Bug#1063837 for it. <https://bugs.debian.org/1063837>