Re: with HTML output, @minus{} is converted to a hyphen instead of a real minus character

[Patrice Dumas]

On Wed, Oct 12, 2022 at 01:59:12PM +0200, Vincent Lefevre wrote:
> 
> Is it? I cannot see any change in the NEWS file in master.

It was actually a change introduced in the 6.7 release.

-- 
Pat