Make "[source]" link to develop branch on github

[kwankyu]

This is a bug in #37589. I made other small edits.

📝 Checklist

• The title is concise and informative.
• The description explains in detail what this PR is about.
• I have linked a relevant issue or discussion.
• I have created tests covering the changes.
• I have updated the documentation and checked the documentation preview.

⌛ Dependencies

[github-actions]

Documentation preview for this PR (built with commit 1d0343e; changes) is ready! 🎉
This preview will update shortly after each push to this PR.

[mkoeppe]

So this simply completes the change that you said you'd do in #37589 (comment)?

[mkoeppe]

By the way, do you think this would this be easy to do:

• CI doc build: Include link to PR in banner, use PR branch in source links #37759

[kwankyu]

So this simply completes the change that you said you'd do in #37589 (comment)?

If you mean Problem 2 mentioned in the comment, no. This PR fixes a bug so that [source] opens a github page that allows me to edit the source file (previously not worked because the github page was on a tag branch). But still github does not allow me to commit the changes because I am in sagemath/sage, not on my forked repo.

[mkoeppe]

Thanks for the explanation. LGTM.

[kwankyu]

ideally the banner at the top would give a link to the PR instead of saying that it's for the development version.

For that, the PR number should be available to the doc build process. Perhaps the PR number could be added to the version...

But I really don't understand how such a link could be useful... The user typically comes to the doc from the PR.

[kwankyu]

... But still github does not allow me to commit the changes because I am in sagemath/sage, not on my forked repo.

A manual way to be able to commit is (of course) to patch the url (from "sagemath/sage" to "user/sage" :-) before starting to edit.

[mkoeppe]

But I really don't understand how such a link could be useful... The user typically comes to the doc from the PR.

Consider the scenario of users who tend to have too many tabs open in the browser

[kwankyu]

I see. I can also imagine that one opens a doc tab separate from a PR tab, which I often do. In that case, back button does not go to the PR.

[kwankyu]

[#37759] Also the source links should link to the branch of the PR, not the tagged version.

No idea.

[mkoeppe]

I've added a link to #37759 to explain where this information is available

[kwankyu]

Thanks. Thanks for review!