Here’s a quick update with a clarification because the problem-solving document is worded in a way that is not entirely clear (I’ll work on fixing that after we merge this). Basically, everyone has to approve this PR so that we can merge it, but if someone doesn’t leave a github review in 14 days, then their approval won’t be blocking the merge.
Now, some people explicitly abstained, which is totally fine. However:
By approving a PR the dev confirms that they reviewed and understood the proposal, and that they are OK with it.
So, as I see it, clicking Approve doesn’t have to mean that you’re fully an advocate of a rename, just that you’re fine with the change.
Anyway, as of right now nobody requested any other changes (meaning that we’re heading for the merge!), but some people still didn’t leave a github review, which means we’ll have to wait a bit.
To keep it safe, it’ll be 14 days since the voting was restarted. This means that this PR will be merged on October 14th if nobody in the list rejects it or requests more changes.
Because this is a massive change, I’m pinging the reviewers again.@JJ @jnthn @lizmat @maettu @masak @MasterDuke17 @rba @samcv @timo @tony-o @ugexe
