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

Rename syl6sseqr to sseqtrrdi #3789

Merged
merged 2 commits into from
Jan 25, 2024
Merged

Rename syl6sseqr to sseqtrrdi #3789

merged 2 commits into from
Jan 25, 2024

Conversation

jkingdon
Copy link
Contributor

This is in set.mm and iset.mm

This is in set.mm and iset.mm
@wlammen
Copy link
Contributor

wlammen commented Jan 23, 2024

The diff looks ok and would usually be approved by me. In the current situation with so many open pull request, I am bit afraid that merging it may cause a lot of conflicts.

@tirix tirix mentioned this pull request Jan 23, 2024
@jkingdon
Copy link
Contributor Author

The diff looks ok and would usually be approved by me. In the current situation with so many open pull request, I am bit afraid that merging it may cause a lot of conflicts.

My general thought process is that merging pull requests quickly when they are ready to go tends to reduce merge conflicts.

But in this specific case, if there is any pull request you particularly think should be merged first, we could do that. I just merged one and looked over the rest (which seemed to me to be in various stages of not being ready), but I'm willing to take requests especially if another pull request seems like it can be merged soon.

@wlammen
Copy link
Contributor

wlammen commented Jan 24, 2024

Perhaps #3781 first?

@jkingdon
Copy link
Contributor Author

Perhaps #3781 first?

Sounds good, we'll see how things go with that one.

@wlammen wlammen merged commit 4d51170 into metamath:develop Jan 25, 2024
10 checks passed
Copy link
Contributor

@wlammen wlammen left a comment

Choose a reason for hiding this comment

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

Approved

@jkingdon jkingdon deleted the sseqtrrdi branch January 25, 2024 13:19
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