@pingou pointed out that in newer releases of pagure, there is a tip on the pull-request page which says git pull https://stg.pagure.io/pagure.git refs/pull/7/head.

That was added in 0c17876 to fix #2823.

Using git pull will likely lead users to merge conflicts. I think using git fetch into a new branch is more friendly. I can add something like this in a follow up patch:

diff --git i/pagure/templates/pull_request.html w/pagure/templates/pull_request.html
index 500590c3..8c17f826 100644
--- i/pagure/templates/pull_request.html
+++ w/pagure/templates/pull_request.html
@@ -660,7 +660,7 @@
       {% if pull_request %}
       <div class="small">
         <p>Pull this pull-request locally <a href="#" id="local_pull_info_btn">v</a></p>
-        <pre id="local_pull_info" style="display:none">git pull {{ config.get('GIT_URL_GIT') }}{{ repo.fullname }}.git refs/pull/{{ pull_request.id }}/head</pre>
+        <pre id="local_pull_info" style="display:none">git fetch {{ config.get('GIT_URL_GIT') }}{{ repo.fullname }}.git refs/pull/{{ pull_request.id }}/head:pr{{ pull_request.id }}</pre>
       </div>
       {% endif %}
     {% endif %}

I'm not sure if there's room in the UI to add && git checkout pr{{ pull_request.id }} to that tip or not. Thoughts?

I like the change and +1 for the patch to the template as well :)

Could you rebase on the top of master while you do this change? (I try to keep the history linear :))

Sure. I squashed the template change into the same commit, since I think it belongs with the documentation update rather than as a separate commit. I can split it out though, if you like even more granular commits. :)

Thanks!

That works for me, thanks ! :)