Hi Sheng,
I suggest to put down a reason for such actions later. It may confuse other
contributors, e.g., Steffen raised his concern in a private thread.
Best
Mu
> On Jun 10, 2018, at 7:42 PM, Sheng Zha wrote:
>
> Thanks, Henri. I was reverting the commit on a PR that another committer
>
Thanks, Henri. I was reverting the commit on a PR that another committer
didn't intend to merge but only realized afterwards. Given that it wasn't
convenient for him to revert and the negative effect, I committed the
revert and cc'd the original committer in the PR, both as notification and
as a
It wasn't clear why this was commit was reverted. Things that stood out as
odd:
* I didn't see an email to dev@ on the topic of a revert.
* Rather than reverting, if there is a minor item requiring a fix it could
simply be fixed; if a major item then it should be raised on dev@.
* I didn't see a
