Subject: Re: bug#59262: Dash instead of two hyphens in manual

From: Antonio Diaz Diaz <[email-masked]>
Date: Tue, 15 Nov 2022 15:56:57 +0100

Thank you Paul and Pádraig for the quick and comprehensive fix! Way beyond 
what I noticed and reported, in fact.

Antonio.