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

there is something wrong with the abbreviations, so that the MMT plugin dies. #12

Open
kohlhase opened this issue Jul 4, 2019 · 2 comments
Open

there is something wrong with the abbreviations, so that the MMT plugin dies. #12

kohlhase opened this issue Jul 4, 2019 · 2 comments
Assignees
@Jazzpirate
Labels
bug Something isn't working

Comments

@kohlhase
Copy link
Member

kohlhase commented Jul 4, 2019

Dennis experienced this in today's KRMT Lab.

And while we are at it, we should have abbreviations
jcalU for jU and something systematic for jC as well.
@kohlhase kohlhase added the bug Something isn't working label Jul 4, 2019
@jfschaefer jfschaefer mentioned this issue Jul 12, 2019
Merged
@jfschaefer
Copy link

I looked a bit into this.
I've created a pull request at UniFormal/MMT#480 that should add all the mathcal and mathbb capitals to the abbreviations.

While testing, I noticed that the abbreviations file had been moved and renamed in MMT since the last release. So the plugin currently can't find the abbreviations file in the MMT jar if it is built from devel.

@ComFreek
Copy link
Member

ComFreek commented Dec 12, 2019 •
edited
Loading

I assume this has been fixed since July since I haven't encountered this issue anymore (in fact not at all)?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@Jazzpirate Jazzpirate

Labels
bug Something isn't working
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@ComFreek @kohlhase @jfschaefer @Jazzpirate