On Fri, Apr 12, 2024 at 12:42:51PM +0200, ???? ??????? wrote: > ping :) Ah thanks for the reminder. I noticed it a few days ago and I wanted to ask you to please include a commit message explaining why it's no longer necessary. We don't need much, just to understand the rationale for the removal.
If you just send me one or two human-readable sentences that can be copy-pasted in the message, I'm willing to do it myself to save you from resending. Thanks, Willy
