Skip to content

Build process disrupted by mkdocs tags_file #1425

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

Closed
mhayter opened this issue Feb 16, 2025 · 3 comments
Closed

Build process disrupted by mkdocs tags_file #1425

mhayter opened this issue Feb 16, 2025 · 3 comments

Comments

@mhayter
Copy link
Contributor

mhayter commented Feb 16, 2025

Config value 'plugins': Plugin 'material/tags' option 'tags_file': This setting is not required anymore
@adamant-pwn @jakobkogler

@jakobkogler
Copy link
Member

jakobkogler commented Mar 9, 2025

I've removed that deprecated option, and used the new correct syntax for the tag index.
Builds work again.

@mhayter
Copy link
Contributor Author

mhayter commented Mar 14, 2025

Unfortunately,when I've rerun build (when I could), it still fails.

@mhayter mhayter reopened this Mar 14, 2025
@jakobkogler
Copy link
Member

jakobkogler commented Mar 15, 2025

@jxu @mhayter
The build works.

Why rerunning some builds doesn't work automatically, is due to technical decisions by Github.

The build step doesn't automatically use the code from the main branch. It actually uses a combination (Git Merge) of the PR and the main branch to the time when the pull request was opened.
So for all the PRs that were opened before my fix last week, the builds use still the code of the old main branch.

That sounds a bit odd. Especially when you come from other Code Versioning / DevOps platforms. E.g. I currently work a lot with Azure DevOps, and there the build always runs on the merge between the most recent target branch and your PR branch.
But I guess Github made the decision to use the creation time as a merge base, because lots of repositories have lots of PRs.
And you don't want to rerun all builds (costs saving), just because the main branch changed.


Anyway. There are two easy solutions.
You can just merge the current main branch into the PR:
Image

Or alternatively close and reopen the PR (which is nicer to the creator of the PR, as they will not have additional commits in their Fork/Branch):
Image

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

No branches or pull requests

2 participants