Skip to content

chore: update button text from 'Leave World' to 'Home'#127

Merged
joneugster merged 1 commit into
leanprover-community:mainfrom
he7d3r:chore/home-button-text
Mar 1, 2026
Merged

chore: update button text from 'Leave World' to 'Home'#127
joneugster merged 1 commit into
leanprover-community:mainfrom
he7d3r:chore/home-button-text

Conversation

@he7d3r

@he7d3r he7d3r commented Feb 14, 2026

Copy link
Copy Markdown
Contributor

This is a follow-up to #120, to update "Leave World" to "Home" everywhere.

@joneugster

Copy link
Copy Markdown
Collaborator

Thanks!

@joneugster joneugster merged commit 6367e71 into leanprover-community:main Mar 1, 2026
1 check passed
@he7d3r he7d3r deleted the chore/home-button-text branch March 2, 2026 10:33
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