I am probably doing something wrong, but when I try using eimm it doesn't like the .mmp saved by mmj2.
the labels are expected to be purely numeric, while the autogenerated labels have a 'd' prefix. it also fails to ignore * comments I'm not sure how other people are using mmj2, and how they export/import... Greetings, Ludwig -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/207d31b0-3426-4620-8d78-089967874e72n%40googlegroups.com.
