Hi Mike, On 11/12/19 03:55, Michael D Kinney wrote: > EDK II Maintainers, > > EDK II CI Phase 1 feature is now active on edk2/master. > > Please use a GitHub pull request from a branch in a personal > fork of the edk2 repository with a 'push' label to request > a set of patches to be pushed to edk2/master. The GitHub PR > replaces the 'git push' operation currently used to commit > changes to edk2/master. > > You will need to configure your notifications from the edk2 > repository to make sure you receive email notifications > when the checks against the GitHub PR passes or fails. > > If you submit a GitHub Pull Request without the 'push' > label, then the CI checks are run and the results are > generated. > > Please let us know if there are any questions about this > change in the development process.
I think this workflow feature has been working well; thank you (and everyone else involved) again for implementing it. Having read a good number of the emails sent out by github.com about such Pull Requests, I'd like to request a new feature, or at least to suggest a usage convention. The presence of the "push" label decides whether the PR is actually meant for master, or if it's a personal build (usually employed as a sanity check before posting a series to the list for review). This difference is important, but there is no sign of the "push" label (or of its absence) in the emails that github.com generates, as far as I can tell. Right now I can only tell the difference from the final mergify bot comment that says - "Merged #197 into master." versus - "All checks passed. Auto close personal build." Can we please - either tweak github.com to include any labels that are tacked to the PR, in the notification emails, - or adopt a convention where "personal build" PRs are required to state that fact in the PR title? Thanks! Laszlo -=-=-=-=-=-=-=-=-=-=-=- Groups.io Links: You receive all messages sent to this group. View/Reply Online (#51266): https://edk2.groups.io/g/devel/message/51266 Mute This Topic: https://groups.io/mt/53725670/21656 Group Owner: devel+ow...@edk2.groups.io Unsubscribe: https://edk2.groups.io/g/devel/unsub [arch...@mail-archive.com] -=-=-=-=-=-=-=-=-=-=-=-
