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.

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

Zermelo #3111

Merged
merged 2 commits into from
Aug 22, 2021
Merged

Zermelo #3111

merged 2 commits into from
Aug 22, 2021

Conversation

pleroy
Copy link
Member

@pleroy pleroy commented Aug 22, 2021

Having Grothendieck/Haar as a marker for the changes done in Entwurf is getting annoying now that it's clear that it's not going in either Grothendieck or Haar, but some other changes do go in Grothendieck and/or Haar. I am using Zermelo as a marker for the changes in Entwurf.

#2400 always takes longer than you expect.

@eggrobin eggrobin added the LGTM label Aug 22, 2021
@pleroy pleroy merged commit 3348e19 into mockingbirdnest:Entwurf Aug 22, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants