@UncombedCoconut one month later, but thanks a lot for trying some numbers (in addition to fixing the issue in the first place)! I'll see if I can find the time to measure it a tiny bit more consistently (inserting a timer around the relevant parts), but your numbers suggest that #2747 isn't useful anymore (which, despite the effort I put into, I'd be happy to get rid of). Anyway, it doesn't seem like having it in slows anything down measurably, so there's no hurry -- but not remembering what it was all about.

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub, or unsubscribe.
Triage notifications on the go with GitHub Mobile for iOS or Android.