On Tuesday, February 11, 2020 at 4:20:57 PM UTC-5, Alexander van der Vekens wrote: > > 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. >
Thanks. That makes our status: job101 assigned to AV, job102-job161 unassigned. > > By the way, PRs for set.mm should not be placed as long as the > minimization is running, should they? > They should be OK as long as they don't have (many) renames, which is why I waited until David's "rng" renaming. Worst case, all that will happen is that a few minimizations might not get applied and will get processed in next year's full run. The final scripts I will use should be robust enough so they will just skip a theorem not found and other errors, and in any case I will be reviewing the log for the final run. So don't worry about it too much. Norm -- 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/b0e8c9e9-3719-4e6b-857a-3fe936cb8543%40googlegroups.com.
