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

Delete irrelevant docs #322

Merged
merged 1 commit into from
Jul 6, 2023
Merged

Delete irrelevant docs #322

merged 1 commit into from
Jul 6, 2023

Conversation

e-lo
Copy link
Collaborator

@e-lo e-lo commented Mar 16, 2023

This PR adds the functionality to delete documentation versions when the corresponding ref (i.e. a branch) is deleted. This will most often occur when a PR is merged and branch deleted. The goal of this PR is to make sure we don't end up with a zillion documentation versions which make it difficult to navigate.

Fixes #321

@e-lo e-lo requested a review from lmz March 16, 2023 00:18
@e-lo e-lo self-assigned this Mar 16, 2023
@e-lo e-lo changed the base branch from master to develop April 10, 2023 16:11
@e-lo e-lo requested a review from i-am-sijia April 10, 2023 16:11
@e-lo
Copy link
Collaborator Author

e-lo commented Jun 14, 2023

ping @i-am-sijia

@e-lo e-lo merged commit 01ee68c into develop Jul 6, 2023
@e-lo e-lo deleted the delete-irrelevant-docs branch July 6, 2023 21:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

[FEATURE] Delete documentation when branch deleted
2 participants