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.

Sign up for GitHub

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

Jump to bottom

Mike for docs versioning #496

Merged
merged 2 commits into from
May 15, 2023
Merged

Mike for docs versioning #496

merged 2 commits into from
May 15, 2023

Conversation

jorisroovers
Copy link
Owner

@jorisroovers jorisroovers commented May 12, 2023 •
edited

Use of mike to publish different versions of the docs

@jorisroovers
WIP: mike for versioning
9db588e 
TODO: needs docs on how to use
@coveralls
Copy link

coveralls commented May 12, 2023 •
edited

Coverage Status

Coverage: 99.661%. Remained the same when pulling ce9ae7d on mike into 5a1cd61 on main.

@jorisroovers jorisroovers changed the title WIP: mike for versioning Mike for versioning May 15, 2023
@jorisroovers jorisroovers changed the title Mike for versioning Mike for docs versioning May 15, 2023
@jorisroovers jorisroovers marked this pull request as ready for review May 15, 2023 08:10
@jorisroovers jorisroovers merged commit 66601ba into main May 15, 2023
42 checks passed
@jorisroovers jorisroovers deleted the mike branch May 15, 2023 08:11
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@jorisroovers @coveralls