Unfortunately I cannot downgrade JDK: the earliest JDK release I can get with "apt" is JDK 11.
I tried to reinstall mmj2, but I get: ........./mmj2/src$ javac `find . ../lib -name *.java` -d ../classes ./mmj/pa/PaConstants.java:121: error: package org.json does not exist So I downloaded json-20190722.jar but I do not know how to make javac understand that it has to use it... Would it be possible to include the package org.json in the mmj2 distribution, so that it is integrated ? Benoît -- 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/ce397d63-f6ec-4c90-8de1-48a3669c1c61%40googlegroups.com.
