Although we can only merge a pull request when the CI succeeds on the pull-request, the GitHub interface allowed me to push buttons in a way that we have a red commit on the main branch…
It happened because latest commit of main (hence #4) was not merged in #16, and although the latest commit of #16 did pass the CI checks, the merge of #4 and #16 was not passing the CI checks.
This pull-request fixes the CI and finish the work of #16 in the files added by #4. I will see if one of the branch protection rules would have prevented this, or if we should have the discipline of merging main in the pull-request before merging the pull-request in main.
Although we can only merge a pull request when the CI succeeds on the pull-request, the GitHub interface allowed me to push buttons in a way that we have a red commit on the main branch…
It happened because latest commit of
main
(hence #4) was not merged in #16, and although the latest commit of #16 did pass the CI checks, the merge of #4 and #16 was not passing the CI checks.This pull-request fixes the CI and finish the work of #16 in the files added by #4. I will see if one of the branch protection rules would have prevented this, or if we should have the discipline of merging main in the pull-request before merging the pull-request in main.