On Thu, Oct 03, 2024 at 07:06:47PM +0200, Patrice Dumas wrote: > It is indeed not necessary and could very well be reverted, either by > using --- that will become --, or setting code style for the leading --. > I hesitated a lot about whether to discuss the change or not, but in the > end I did not as it seemed to me to fall in the non semantic changes > that we consider, in general to be ok. I probably should have. > > In any case, given what Eli found in the archive, I think that it is > better to revert.
OK, thank you.
