Fix bad Github merge

[erikd]

Description

The changes in PRs #3491 and #3482 turned out to be incompatible.
To avoind things like this, it would be ideal if PRs were not merged unless they were rebased and had a complete CI build first.

Linked issue

N/A

Type of change

• 🐞 Bug fix (non-breaking change which fixes an issue)
• 🛠 New feature (non-breaking change which adds functionality)
• ⚠️ Breaking change (fix or feature that would cause existing functionality to change)
• 🏭 Refactoring that does not change existing functionality but does improve things like code readability, structure etc
• 🔨 New or improved tests for existing code
• ⛑ git-flow chore (backport, hotfix, etc)

Developer checklist

• I have read the style guide document, and my code follows the code style of this project.
• If my code deals with exceptions, it follows the guidelines.
• I have updated any documentation accordingly, if needed. Documentation changes can be reflected in opening a PR on cardanodocs.com, amending the inline Haddock comments, any relevant README file or one of the document listed in the docs directory.
• CHANGELOG entry has been added and is linked to the correct PR on GitHub.

Testing checklist

• I have added tests to cover my changes.
• All new and existing tests passed.

QA Steps

Screenshots (if available)

[edsko]

LGTM.

[CodiePP]

fine with me. I think it is hard to avoid such coincidences.
Now, it just turned green!

[erikd]

I think it is hard to avoid such coincidences.

At my previous employer we had a CI test that only turned green if the PR branch had been rebased against the branch it was being merged to.

[CodiePP]

good point; you should propose it to devops. I am PRO!