Thanks! Patch pushed manually because the one from this PR doesn't have the commit message formatted as per guidelines in contributing.md

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