[jonalmeida]

Seems like we missed doing this.

Pull Request checklist

• Accessibility: The code in this PR follows accessibility best practices or does not include any user facing features

[mergify]

Queue requested — the merge queue status continues in this comment ↓.

[mergify]

🚫 Left the queue · pull request dequeued

Less than a minute in the queue, with no time running CI.

So far

• ✅ Entered the queue Sat 7 Nov, 01:35 · rule default · triggered by @jonalmeida with the merge queue checkbox
• ✅ Checks skipped · PR is already up-to-date
• 🚫 Left the queue 01:36 · 854fcb4

Reason

Pull request #4645 has been dequeued

GitHub refused to merge the pull request. At least 1 approving review is required by reviewers with write access. This is usually enforced by a branch protection or ruleset rule.

To get back in the queue

• Push a change if one is needed: the pull request is queued again once its queue conditions match.
• If no change is needed, tick the box below to queue it again as it is.

Requeue requested — the merge queue status continues in this comment ↓.

1 merge condition met

• status-success=pr-complete

_{Times in UTC · dashboard · how the merge queue works}

[rvandermeulen]

@Mergifyio queue

[mergify]

✅ Merged into master as 8e08429 at 19:24 UTC

18 min in the queue, 17 min of it CI.

So far

• ✅ Entered the queue Sun 8 Nov, 19:06 · rule default · triggered by @rvandermeulen with the @mergifyio queue command
• ✅ Passed · in place
• ✅ Merged 19:24 · 8e08429 · rebase

1 merge condition met

• status-success=pr-complete

_{Times in UTC · dashboard · how the merge queue works}