Skip to content

Stop building the CodeQL for VS Code docs now they've been migrated #16496

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

Merged
merged 4 commits into from
May 17, 2024

Conversation

felicitymay
Copy link
Contributor

@felicitymay felicitymay commented May 15, 2024

This change should stop us building the CodeQL for VS Code docs as part of the docs publication for the CodeQL docs site. It's likely to delete the HTML files from the codeql-docs repository, but I've checked with Rachael and this won't have any impact on the redirects that we already have in place.

This change is worth doing so that, as we hand over more responsibility for the CodeQL docs site to the CodeQL team, there are fewer areas for confusion.

I'll test this PR by running a docs build and creating a test PR to update the CodeQL docs site.

@felicitymay
Copy link
Contributor Author

It turns out that we need to update all the links to the VS Code extension before we can stop generating the files as part of the Sphinx build, see: https://github.com/github/semmle-code/actions/runs/9092490831/job/24989320159.

@felicitymay felicitymay marked this pull request as ready for review May 15, 2024 13:16
@felicitymay felicitymay added the ready-for-doc-review This PR requires and is ready for review from the GitHub docs team. label May 15, 2024
Copy link
Contributor

@subatoi subatoi left a comment

Choose a reason for hiding this comment

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

Many thanks for putting this together, @felicitymay

@felicitymay felicitymay merged commit daf19a2 into main May 17, 2024
@felicitymay felicitymay deleted the felicitymay/sphinx-config branch May 17, 2024 12:37
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
documentation ready-for-doc-review This PR requires and is ready for review from the GitHub docs team.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants