Thanks David for this work. I have two down-to-earth questions: * When linking to a page in the metamath website (or when sending a link to someone), we should always use "https://us.metamath.org/..."; (that is, "https" and "us" as opposed to "http" and "us2", and no port indication like ":88" as is the case for us2). Correct ?
* When is the website updated after a PR is merged ? (e.g., "the following day at 6pm GMT", or "within the following 12 hours", or...) ? Or does it vary ? Maybe different pages have different refresh rates ? Thanks, Benoît On Tuesday, August 30, 2022 at 5:53:56 AM UTC+2 David A. Wheeler wrote: > I *think* I've worked out the other problems in > having us.metamath.org generate the metamath website. > I'm going to re-run a test from scratch. > > If it all works, then within the next few days I intend to *disable* the > website > generation by us2.metamath.org, and switch over to using us.metamath.org > to both generate AND serve web pages. When I do that, I'll let everyone > know. > At that point, please let me know if there's an unexpected problem. > > I intend to keep the old us2.metamath.org on standby mode in case there's > a problem, so we can switch back to using it. Once we confirm that > the new system is working well, we can work on updating how the > mirrors get their information. > > *Hopefully* this is one step closer to decommissioning Norm's old machine. > > --- David A. Wheeler > > -- 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/627fe73a-c87d-481a-a86e-a752da1b9e91n%40googlegroups.com.
