Probably most people who have contributed to metamath have noticed the
way that our rewrapping scripts and practices tend to lead to things
like generating diffs in your pull request which are unrelated to the
change you are making (because the last person didn't rewrap and you
did, typically).
After some consultation between Benoit, Mario and me (and maybe others
in the past), we have changed the github checks so that a pull request
must have run rewrap into order to pass the automated checks. If your
pull request fails this check, you just need to run scripts/rewrap and
push the results, which should fix the failure.
I've updated the
https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md file
with the following text: "On pull requests we check that set.mm and
iset.mm have been rewrapped to help conform to their formatting
conventions. Locally you will need to run |scripts/rewrap set.mm| to
avoid failing this check." Although the commands which had been listed
there are still perfectly fine, my intention is that the only thing you
need to worry about is scripts/rewrap. I'm hoping that among other
things this will be easier for new contributors, who just have to deal
with "how do I fix this failing build?" and not "here are some rules
which are written but not enforced and if you don't do it that's OK but
others will kind of wonder what happened and maybe it is only sort of
OK" which is roughly the situation we have been in, as I see it.
If there are any questions or concerns, just ask (for example, here or
on https://github.com/metamath/set.mm/issues/2381 ). We can always
change this again if people don't like it, I can help explain how it now
works, etc.
--
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/35fb2a49-f338-c025-1cdc-3e88a197ce76%40panix.com.
