Thanks for the explanation, Norm. Glauco
Il giorno sabato 22 agosto 2020 alle 19:47:28 UTC+2 Norman Megill ha scritto: > The comment at the top of set.mm says, "To prevent GitHub merge > conflicts, please change the above date only if there are no other pull > requests in the queue." Since merge conflicts caused by this been a > problem, the Travis check uses the "/top_date_skip" qualifier for "verify > markup" so that updating the top date is optional. You can use that > qualifier locally. > > It has been suggested that we remove the top date, but I like it for my > personal use. Whenever I come across a set.mm copy in some old directory > or backup, "head -1 set.mm" will tell me the version more reliably than a > directory time stamp that "cp" without "-p" will destroy. Usually the > submitter of the first PR in the queue updates the date, but if not at > least it's usually pretty close. If two people change the top date to > different values (due to time zone differences) I'll typically fix the > conflict myself before merging the second PR, not a big deal. > > Norm > > On Saturday, August 22, 2020 at 12:44:25 PM UTC-4 Glauco wrote: > >> I've just pulled the latest set.mm and launched a verify markup. >> >> I get this error >> The "Version of" date 19-Aug-2020 at the top of file >> ".../git/set.mm/set.mm" is less recent than the date >> 21-Aug-2020 in the description of statement "imadifss" >> >> I've also checked the version online and it confirms the apparent >> inconsistency. >> >> Shouldn't Travis have prevented this? (sorry if I'm missing something >> simple) >> >> Glauco >> > -- 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/9145b4d5-4c72-4380-8569-5fe805f802e8n%40googlegroups.com.
