PR checkout commands

[delvh]

Feature Description

GitHub offers a dropdown to the right of a PR title to copy the checkout instructions for said instructions.
Gitea could offer the same with the only difference being instead of the GitHub CLI,
a) Agit-Flow with the command (I hope I understand the agit-flow commands correctly)

git download $PR_ID

b) Pure Git with the command

# Assumes you named the remote host origin
git fetch origin pull/$PR_ID/head:$BRANCH_NAME_AS_NAMED_BY_PR_CREATOR && git switch $BRANCH_NAME_AS_NAMED_BY_PR_CREATOR

Alternatively, to be on the save side regarding potential name conflicts:

# Assumes you named the remote host origin
git fetch origin pull/$PR_ID/head:pr-$BRANCH_NAME_AS_NAMED_BY_PR_CREATOR && git switch pr-$BRANCH_NAME_AS_NAMED_BY_PR_CREATOR

are provided.

Screenshots

Display on GitHub:

[noerw]

tea pr checkout <idx> is also an option

[lunny]

So we should also add a tea command instructions on the PR page near git one.