Closed jvoisin closed 1 year ago
This is a duplicate of #232, but thanks for the reminder.
Oops, you're absolutely right, sorry for the noise.
@jvoisin Maybe this is your opportunity to contribute a fix, although the related code review I suggested in #232 is non-trivial.
I get the following warnings on eaf83476463e22b065a0ab9ee896fd1a563fc44d. Nothing horrible, but it would still be nice to get it fixed or silenced.