Could someone summarize the design changes required in an issue on the metamath-exe repo? I think I know how to do the change but I'm not sure what flags we're adding or deleting or how the defaults change.
On Sun, Jan 2, 2022 at 10:22 AM Benoit <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/7979554e-9af8-4fc2-8d16-295e09b4c662n%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/CAFXXJSs-jgcQJ1rTWG7Xjgw-gSqQKTGHEzaD5sqEPAYaytPHYg%40mail.gmail.com.
