Hi, The images in your email are not displaying for me. Can we run these security/quality checking tool locally? I am not sure we should block all PRs based on new CVEs being released which may require lots of work to upgrade dependancies.
Thanks -----Original Message----- From: Simon Steiner <[email protected]> Sent: 07 March 2023 20:50 To: [email protected] Subject: RE: [GitMigration] Rename Git Mirrors for XML Graphics Project Hi, We are seeing so many emails after using the PR system today that its hard to review changes. Thanks -----Original Message----- From: Simon Steiner <[email protected]> Sent: 07 March 2023 20:49 To: [email protected] Subject: RE: [GitMigration] Rename Git Mirrors for XML Graphics Project Hi, I think the overhead it adds, issues arounds CI failing for reasons outside of your control. Can you rerun github pr ci if it fails. If your changing something that wont affect CI such as a small typo, documentation? For large changes it is good to open a code review. Thanks -----Original Message----- From: Glenn Adams <[email protected]> Sent: 07 March 2023 20:33 To: [email protected] Subject: Re: [GitMigration] Rename Git Mirrors for XML Graphics Project I haven't done that yet, though I would like to do so. There are a variety of reasons for requiring PRs, including - ensure that GitHub actions, such as build, test, analyze, are completed (in PR branch) successfully before merging into main - ensure that PR conversation (including discussion resolution) and changes are recorded and retained for future reference - enable (optional) review processing, should it be desired Given that it takes only a few mouse clicks in GH to create a PR from a commit on a private branch, is there any reason we shouldn't use PRs for all prospective merges? We should take advantage of the tools gained from migrating to Git, yes? On Tue, Mar 7, 2023 at 12:47 PM Simon Steiner <[email protected]> wrote: > Glenn are you making PRs required for the git repos, should this go > thru a vote before being implemented? > --------------------------------------------------------------------- To unsubscribe, e-mail: [email protected] For additional commands, e-mail: [email protected]
