Anton Trunov (May 13 2020 at 07:13): Anton Trunov (May 13 2020 at 07:13):I have a question about the workflow in the case of merging PRs with backwards compatible overlays. Should the PR author remove the overlays before the PR can be merged? I couldn't find this in the contributing guide.
Enrico Tassi (May 13 2020 at 08:01):I seem to recall that the recommended way is to have the overlay PRs merged before the PR is (being retro compatible). If all are merged then the overlay itself could be removed from the main PR before merging. I don't recall this being mandatory, but it results in a CI run that ensures all PR were actually merged, so it seems a nice thing to do. For sure it will spare the assignee the work of going to each PR an say "please merge" ;-)
Anton Trunov (May 13 2020 at 08:04):but it results in a CI run that ensures all PR were actually merged, so it seems a nice thing to do.
My thinking precisely! Thank you Enrico. I guess I'll open a PR with this suggestion to make the discussion more formal.
Last updated: Oct 01 2023 at 19:01 UTC