Skip to content

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

@mkoeppe

Description

@mkoeppe

For HTML documentation built from PRs, ideally the banner at the top would give a link to the PR instead of saying that it's for the development version.
(Example: https://deploy-preview-37714--sagemath.netlify.app/html/en/reference/arithgroup/sage/modular/arithgroup/congroup_sl2z)

Also the source links should link to the branch of the PR, not the tagged version.

The necessary information is available in environment variables such as GITHUB_SERVER_URL, GITHUB_REPOSITORY, GITHUB_REF , GITHUB_SHA https://docs.github.com/en/actions/learn-github-actions/variables#default-environment-variables

And there could be a link to the CHANGES file.

Originally posted by @mkoeppe in #37589 (comment)

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions