Based on #41 (comment), we should have a GitHub workflow that ensures that every pull request has the necessary labels and milestones. This can later be set up as a requirement that has to be met before a pull request can be merged.

Here's the specifications that the GitHub workflow should implemented (based on #41 as well):

• Every pull request must have one of the [Type] xyz labels. This is used to group pull requests in the changelog.
• Every pull request must have either one of the [Focus] xyz labels or the Infrastructure label. This is used to further categorize and prefix pull requests in the changelog.
• Every pull request must have either a milestone set or be marked with the no milestone label. This is used to define which release a pull request belongs to, or to explicitly define that a certain issue is "release-irrelevant" and therefore does not need a milestone.