Agreed, the extra coverage here is probably not worth the additional CI cost for such a small fix.
I'll drop this patch. Thanks for the review.
Agreed, the extra coverage here is probably not worth the additional CI cost for such a small fix.
I'll drop this patch. Thanks for the review.