Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use Remotes.GitHub when building docs to show link to repo in navbar #83

Merged
merged 1 commit into from
Jan 31, 2024

Conversation

JoshuaLampert
Copy link
Owner

@JoshuaLampert JoshuaLampert commented Jan 29, 2024

There are warnings when building the docs because Documenter.jl is unable to determine the repo URL. Using Remotes.GitHub should fix this so that the link to the repo is shown in the upper right in the documentation.

@JoshuaLampert JoshuaLampert requested a review from ranocha January 29, 2024 16:20
@JoshuaLampert JoshuaLampert enabled auto-merge (squash) January 29, 2024 16:22
Copy link
Collaborator

@ranocha ranocha left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@ranocha ranocha disabled auto-merge January 31, 2024 12:53
@JoshuaLampert JoshuaLampert merged commit bc3020d into main Jan 31, 2024
3 checks passed
@JoshuaLampert JoshuaLampert deleted the docs-Remote-GitHub branch January 31, 2024 12:53
@ranocha
Copy link
Collaborator

ranocha commented Jan 31, 2024

You need to merge this manually since some required checks don't run for pure docs changes like this. (I don't have the rights to force-merge this PR)

@JoshuaLampert JoshuaLampert added the documentation Improvements or additions to documentation label May 5, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
documentation Improvements or additions to documentation
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants