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/2c1caa31-83b5-40d3-8d5c-1a09b19335b4n%40googlegroups.com.
