The version date of set.mm is less recent than the contribution date for imadifss

[Glauco]

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

[Norman Megill]

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

[Glauco]

Thanks for the explanation, Norm.

Glauco