On 04/05/2023 10.02, Axel Beckert wrote:
Actually its even more embarrassing: A patch for that is already in Git, albeit a bit less elegant and maybe less performant:
But perhaps more correct. This should probably not be limited to --ignore-obsolete.
Andreas