This is the result of https://github.com/metamath/set.mm/pull/2392
In MM, it suffices to type "MM> v m */t/f" to obtain the "top_date_skip" and "file_skip" behavior. I guess this behavior should eventually be made default (while keeping the useless options /top_date_skip and /file_skip for compatibility), and options /top_date_check and /file_check should be created. Benoît On Sunday, January 2, 2022 at 4:13:09 PM UTC+1 [email protected] wrote: > No, because CI runs scripts/verify --top_date_skip which includes VERIFY > MARKUP * / TOP_DATE_SKIP > On 1/2/22 4:42 AM, Glauco wrote: > > Running a "verify markup" with a recent set.mm I'm getting a > > There is no "Version of " comment at the top of the file > > warning. It looks like the date is not at the top of the file anymore (as > it was discussed some time ago, in this forum). > > I'm on Version 0.198 7-Aug-2021 , that's the current one (according to the > metamath.org page). > > I've checked > https://github.com/metamath/metamath-exe/releases > but there aren't any releases, yet. > > Will CI block my PR ? > > Glauco > > > Il giorno venerdì 31 dicembre 2021 alle 05:57:53 UTC+1 [email protected] > ha scritto: > >> This is to give more visibility to issue >> https://github.com/metamath/metamath-exe/issues/19 . This came up when I >> put a .gitignore in the metamath-exe repo: We currently distribute the >> metamath sources via tar file, and it would be odd to distribute the >> .gitignore as well. >> >> I think we should move to a release process entirely hosted on github, >> with the web site pointing to the >> https://github.com/metamath/metamath-exe/releases page, which will be >> semi-automatically populated with releases built in CI. >> > -- > 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/d1f1e874-d61f-4d80-a8bc-96bfbc0e5f38n%40googlegroups.com > > <https://groups.google.com/d/msgid/metamath/d1f1e874-d61f-4d80-a8bc-96bfbc0e5f38n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > > -- 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/7979554e-9af8-4fc2-8d16-295e09b4c662n%40googlegroups.com.
