Folks, I tried to push some trivial commits directly to the master branch and was surprised that is no more allowed.
The error message is not crystal clear, but I guess the root cause is the two newly required checks (Commit email checker and Signed-off-by-checker) were not performed. As a kind of workaround, I created a PR so these two checks can be performed and the commits marked as good, and then fast forwarded my master branch and pushed it into master. I do not think these checks can be performed "on the fly" by the GitHub servers, so if they are marked as required, it means it is no more possible to push directly to master. Is this a behavior we expected ? If not, are we fine with it ? Generally speaking, should we always issue PR and use the GitHub merge button ? /* note if the commit is trivial, then it is possible to add the following line [skip ci] into the commit message, so Jenkins will not check the PR. */ Cheers, Gilles _______________________________________________ devel mailing list devel@lists.open-mpi.org https://lists.open-mpi.org/mailman/listinfo/devel
