gh-pages deployment with material theme #2966
Merged
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.
So this PR does several things. The point is to migrate to gh-pages, as it allows us to use any theme we want, which enables us to move forward with the idea of improving the look&feel of the mongooseim documentation.
This documentation is generated using
mike
, which, using mkdocs and material, enables us to build several versions, tagging them and pushing them.How mkdocs generate these sites? Compiling all the markdown files and the mkdocs.yml into a huge bunch of static html and css files. mike injects some minor javascript then to allow to change versions. These lots of autogenerated files are then pushed to a github repo that github allows to serve as static pages. But the amount of autogenerated stuff is too big to keep in our main repo, so these things are pushed to a new repo we've made, https://github.com/esl/MongooseDocs.
More things that this PR does: migrating all links to readthedocs to our new pages, improving some http-to-https links (my firefox complained about that), improving some minor indentation and whitespace in doc files, and, importantly, adding building docs to the CircleCI pipeline. All branches will be built, but only tags and master will then be pushed.