Hi Norm, I accidentally picked job101 and started it. It's (still) running. I'll send you the job101.log file after the job has finished.
By the way, PRs for set.mm should not be placed as long as the minimization is running, should they? Alexander -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/37407db1-db05-481b-bbe2-b986366297ae%40googlegroups.com.
