refs/pull/##/head is not updated after a Rebase and merge

[InExtremaRes]

• Gitea version (or commit ref): b9ae16d

(using Gitea in Docker with image of Id: "sha256:73bd5621a03339e79b4ef48392aeb68be5eedff40c068763f0d7f73f866a233c")

• Can you reproduce the bug at https://try.gitea.io:
  • Yes https://try.gitea.io/inextremares/testing/graph
  • No
  • Not relevant

Description

When a PR is merged using Rebase and merge, commits are rebased but the branch and ref to the PR (refs/pull/#/head) is not updated but left behind in previous commit. I don't know if this will also happen with #4052.

If I update the branch manually (via rebase or reset, and push --force) the branch is updated but the PR and the ref is not. I assume because the PR is closed after merging.

Edit

I was recently trying the same in github (there is no commit graph AFAIK but I pull directly with git fetch remote pull/n/head:local) and the ref is also not updated after the Rebase and merge. So I think this is expected behaviour? In that case, can someone explain me (or point to a doc) why?

Screenshots

Here you can see how the ref and branch is left behind after the Rebase and merge (take attention to the commit with message fix spell)

[stale]

This issue has been automatically marked as stale because it has not had recent activity. It will be closed if no further activity occurs during the next 2 weeks. Thank you for your contributions.

[stale]

This issue has been automatically closed because of inactivity. You can re-open it if needed.