Apply a delay before we enable auto merge on a PR (#992)

We saw the auto merging workflow (added in
#988) failed in
https://github.com/mmtk/mmtk-core/actions/runs/6587030083/job/17896533403.
The error message was `GraphQL: Head branch is out of date. Review and
try the merge again. (mergePullRequest)`. It is likely caused by the
issue https://github.com/orgs/community/discussions/24462: When a PR
gets updated, Github has a process to determine if the PR is mergable.
If we attempt to enable auto merge before the process is done, the merge
will fail with the error message above. This PR adds a delay and retry
for enabling auto merging.

.github/workflows/auto-merge-inner.yml

@@ -87,9 +87,15 @@ jobs:
           git commit -m "Update mmtk-core to ${{ inputs.core_commit }}"
           git push
 
+      # Apply a delay before we attempt to merge and retry if we fail: there is a small period of time that we cannot merge a PR after we update it.
       - name: Enable auto-merge for the PR
         if: steps.check-input.outputs.skip == 'false'
         run: |
-          gh pr merge ${{ steps.get-pr.outputs.pr_number }} --auto --repo ${{ inputs.base_repo }} --squash
+          for n in {1..5}; do
+            echo "Wait 30s then try merge"
+            sleep 30
+            gh pr merge ${{ steps.get-pr.outputs.pr_number }} --auto --repo ${{ inputs.base_repo }} --squash && break
+            echo "Failed to merge the PR. Retry..."
+          done
         env:
           GITHUB_TOKEN: ${{ secrets.CI_ACCESS_TOKEN }}