Thanks! The patch is rather minimal, so I am merging it. Any updates that one may find useful can be made as a new PR.
—
Reply to this email directly, view it on GitHub, or unsubscribe.
You are receiving this because you are subscribed to this thread.