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

Fix issue documentation links. #7687

Merged
merged 1 commit into from
Feb 17, 2022

Conversation

AndrolGenhald
Copy link
Collaborator

I noticed https://psalm.dev/docs/running_psalm/issues/ hadn't updated yet so I ran mkdocs locally to see if it was failing for some reason. It worked, but it had warning messages about these broken links.

@AndrolGenhald AndrolGenhald added the release:docs The PR will be included in 'Docs' section of the release notes label Feb 17, 2022
@orklah orklah merged commit 2e2099e into vimeo:master Feb 17, 2022
@orklah
Copy link
Collaborator

orklah commented Feb 17, 2022

Thanks! My mistake :p

@AndrolGenhald
Copy link
Collaborator Author

@orklah any idea why the docs site isn't updating?

@orklah
Copy link
Collaborator

orklah commented Feb 17, 2022

I never really looked at how it worked, but maybe it retrieve only default branch docs? This was merged in master so it may not be the chosen source

@AndrolGenhald
Copy link
Collaborator Author

I considered that, but it has the docs from #7593: https://psalm.dev/docs/running_psalm/issues/MissingConstructor/
Unless it was changed since that merged it should be using master.

@orklah
Copy link
Collaborator

orklah commented Feb 17, 2022

Maybe it's related to the fact psalm.dev has been updated since: https://github.com/psalm/psalm.dev/commits/master

Maybe it takes that for rebuilding the website?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
release:docs The PR will be included in 'Docs' section of the release notes
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants