Much nicer ! And I even noticed a problem in set.mm thanks to your video: the very early appearance of "Supplementary material.../Mathbox for BJ" is due to my copy-paste error in the comment of bj-equsb1v, which I'm going to fix right now. (There will still be bj-eu3f and bj-eumo0 which are backups of demoted theorems placed in my mathbox.)
Benoit -- 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/423ce59a-9a1c-4f9a-8901-2df0c476cde6%40googlegroups.com.
