Yeah, I don't feel strong on this one either. In the original post it seemed to be reasonable for some people. The original PR is already 4 years old and the original source branch seems to have been removed. Let's close #607 by merging this one or let's close both if it's not going to be merged (would be fine for me also).

What do other people think (merge or reject)?

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