Wolfgang Walther d086c6c6b3 ci/github-script/merge: add hint about stuck GitHub ...

Unfortunately it still happens frequently that, after enabling
auto-merge, GitHub is stuck even though all checks have passed, and
doesn't merge the PR. Any contributor can trigger GitHub again with an
approval of the PR - this will then immediately queue the PR for merge.

Adding a hint to the posted comment, should help users through this
without my intervention.

2025-11-06 15:18:01 +01:00

9.9 KiB

Raw Blame History

View Raw