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

Rename mpt2v , mpt2mpt and mpt2mptx #3395

Merged
merged 3 commits into from
Aug 18, 2023
Merged

Rename mpt2v , mpt2mpt and mpt2mptx #3395

merged 3 commits into from
Aug 18, 2023

Conversation

jkingdon
Copy link
Contributor

  • Rename mpt2v to mpov
  • Rename mpt2mpt to mpompt
  • Rename mpt2mptx to mpomptx

@jkingdon
Rename mpt2v to mpov
a2981fe 
This is in set.mm and iset.mm
@jkingdon
Rename mpt2mpt to mpompt and mpt2mptx to mpomptx
d0de60c 
This is in set.mm and iset.mm
@jkingdon
rewrap
f5d1bbe
wlammen
wlammen reviewed Aug 18, 2023
View reviewed changes
Copy link
Contributor

@wlammen wlammen left a comment •
edited
Loading

Choose a reason for hiding this comment

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

These renamings seem not to conflict with #3389 and #3391, so there is no need to put them on hold, in my eyes.

@jkingdon jkingdon merged commit 4ff3c78 into metamath:develop Aug 18, 2023
9 checks passed
@jkingdon jkingdon deleted the mpov branch August 18, 2023 13:31
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@wlammen wlammen wlammen approved these changes

@avekens avekens avekens approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@jkingdon @avekens @wlammen