Skip to content

Mike default#5

Merged
chenkasirer merged 4 commits into
mainfrom
mike_default
May 18, 2026
Merged

Mike default#5
chenkasirer merged 4 commits into
mainfrom
mike_default

Conversation

@chenkasirer
Copy link
Copy Markdown
Member

@chenkasirer chenkasirer commented Apr 17, 2026

For a first-ever deployment with mike, it's necessary to set a default version. this takes care of the creation of a root-level index.html file which points to it. In the Sphinx workflow this was done by the docversions.

Copy link
Copy Markdown
Member

@gonzalocasas gonzalocasas left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

lgtm!

@gonzalocasas
Copy link
Copy Markdown
Member

we should merge this, right?

@chenkasirer
Copy link
Copy Markdown
Member Author

we should merge this, right?

indeed. sorry, forgot all about it

@chenkasirer chenkasirer merged commit a22ee3a into main May 18, 2026
@chenkasirer chenkasirer deleted the mike_default branch May 18, 2026 07:34
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.

2 participants