You said @ntrel needs to push upstream, but it sounds like it was already diverged, so IMO he doesn't have to do it (inferred "for this PR"), just that ideally "someone" would do it eventually.

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