hol.mm ql.mm demo0.mm miu.mm big-unifier.mm peano.mm have been added in PR 1722 https://github.com/metamath/set.mm/pull/1722 You or a volunteer can update these with the desired CC0 wording. (I won't be doing that myself.)
Norm On Monday, July 13, 2020 at 2:23:16 AM UTC-4, Giovanni Mascellani wrote: > > Hi, > > Il 12/07/20 21:42, Norman Megill ha scritto: > > While I expect all of the .mm's will be kept updated in the > > http://us.metamath.org/metamath/ directory indefinitely, I suggest we > > add the missing ones (hol.mm ql.mm demo0.mm miu.mm big-unifier.mm > > peano.mm) to the https://github.com/metamath/set.mm directory. That > > will put them under version control (they aren't now) and will also be > > guaranteed to be the latest (us.metamath.org sometimes lags by a few > > days). I will do that tomorrow if there are no objections. > > That looks like a good idea to me. > > > Once these are on github, they can be updated via pull requests with > > whatever CC0 wording is desired. > > > > For nf.mm, I would suggest making a PR with the desired changes, then > > wait for Scott Fenton's (@sctfn) approval (if he isn't reading this post > > now). > > Ok, thanks for the suggestions. > > Giovanni. > -- > Giovanni Mascellani > Postdoc researcher - Université Libre de Bruxelles > > -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/d634f168-a4df-4c54-b80f-5fc7856713b5o%40googlegroups.com.
