Brian,
We will address.
пт, 7 июля 2017 г. в 14:25, Barrett, Brian via devel <
devel@lists.open-mpi.org>:
> Hi all -
>
> Earlier this week, we discovered that a couple of pull requests had been
> posted against the deprecated v3.x branch (instead of the active v3.0.x
> branch). Worse, Github all
Hi all -
Earlier this week, we discovered that a couple of pull requests had been posted
against the deprecated v3.x branch (instead of the active v3.0.x branch).
Worse, Github allowed me to merge those requests, despite Github reporting that
nobody had permissions to write to the branch (oddl
FYI: the "signed-off-by-checker" CI on Github now ignores merge commits
(because those usually aren't signed -- e.g., if you file PR A against an
existing PR B, when someone merges A into B, there's now a merge commit on B).
Previously, the signed-off-by-checker would flag such merge commits as
