Therefore thanks for putting time in it even though it wasn't your PR originally 👍

My pleasure.

Once the others agree to merge it, the only thing left to do would be to squash the commits into one.

Done.

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub, or mute the thread.