Remove mdbook #839
Merged
Remove mdbook #839
+37
−568
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
carlostome
force-pushed
the
carlos-remove-mdbook
branch
from
489c805 to
d8e769b
Compare
carlostome
force-pushed
the
carlos-remove-mdbook
branch
from
d8e769b to
9fecb1e
Compare
In particular, we need to keep the js path in the build_config, otherwise we won't have the nice colors in dark mode. Also, I think we should either continue to have an `md/common` (and put there everything that could be used in other web platforms) OR put everything under `md/mkdocs/docs` (e.g., `css/custom.css` and `js/custom.js`), but I don't think we should have an `md/common` that only contains just *some* of the common stuff.
williamdemeo
approved these changes
Sep 26, 2025
There was a problem hiding this comment.
I ran the pipeline and checked the resulting web site. I fixed some things that broke (e.g., Agda colors in dark mode; a missing reference due to a bad path to ConwayBootstrap.md and ConwayBootstrapEnact.md) and rearranged it so basically all the static web stuff is under mkdocs, since it's seemed you had gone most of the way to that end. Everything seems to be working now. Nice work! LGTM
but we do need md_js_dir (for katex-config.js)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description
Cleans mdbook from the repository.
common/srctomkdocs/docsChecklist
CHANGELOG.md