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

MPS-33490: using the 'subscript' script-kind style is non-intuitive #62

Closed
wants to merge 1 commit into from
Closed

Conversation

aamt74
Copy link
Contributor

@aamt74 aamt74 commented Aug 3, 2021

@maros-sandor Thanks for the feedback. I changed the name to "super/subscript", and modified it the proper way now.

I cannot get master to work after the recent bump to 2021.2. It seems that master currently undergoes a lot of active development. To no longer delay this issue, I made the change against HEAD of 2021.1. I hope that is alright.

@maros-sandor
Copy link
Contributor

maros-sandor commented Sep 15, 2021

I can see the merge already got into the public MPS repo. Can you update your repo as well? I think github should then close this request as merged. It may not happen though in case it checks the destination branch is exactly 2021.1.

@aamt74 aamt74 closed this Sep 16, 2021
@aamt74 aamt74 deleted the MPS-33490 branch September 16, 2021 07:17
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