Norm, thank you for tagging v0.182 as well as merging the pull request. I am getting the impression that this thread has mostly increased your maintenance burden. That's really counter to my intent and needn't be the case!
The whole release process on the GitHub side can be made very automatic. It could boil down to a single git command on your end that pushes a commit, triggering Travis, which then publishes a tar release if everything checks out or emailing you if Travis encounters a problem. If this kind of thing sounds worthwhile, I would be willing to help set it up! Cheers, "David A. Wheeler" <[email protected]> wrote: > > On Monday, April 27, 2020 at 3:11:43 AM UTC-4, heiphohmia wrote: > > ... > > >Previously, at the 0.181 update Giovanni asked you to incant the > > >following: > > > git commit -m'Release version 0.181.' > > > git tag v0.181 > > > git push > > > git push --tags > > Yes, that will work just fine for tagging a version and distributing it via > GitHub. > Lots of software is distributed this way. Then anyone can get, for example, > the source code of version 0.182 as a .tar.gz file via: > https://github.com/metamath/metamath-exe/archive/v0.182.tar.gz > It git parlance these are "lightweight tags" and should be fine for the > purpose. > > Once a particular source code version has a particular tag, that tag > should always refer to that specific version of the source code for all time. > You can modify the software, of course, just give the new version a new tag. > This is what the Linux distributions want: a URL that always gives exactly > the same version of the software. That way they can do rebuilds, etc. > > If you forget to tag a release, you can add a tag to an old version this way: > git tag -a vWhATEVER SHA-OF-COMMIT > git push --tags > > However... on GitHub "releases" and "tags" are related but not exactly the > same thing. > Here's my attempt to de-confuse, and I've mis-stated something please let me > know. > GitHub is one of many systems that build on git. Git has tags built-in. > GitHub has an *additional* concept called a "release"; that is > GitHub-specific. > A "release" is intended for releasing binaries built from a tagged instance. > To create a release, you must first create a git *tag* of the source code > as described above. Then, to create a release, you identify the git tag, and > add whatever files you want (generally these are compiled executables, like > the compiled result from source code). > > What confuses things further is that on GitHub, to see the list of tags OR > releases, > you click on the little word "releases". You can then select between the tab > that lists tags, or the tab that lists releases. It's confusing. > > The Linux distros don't want your prebuilt compiled code, just the source > code, > so using git tags should be quite fine. > > --- David A. Wheeler -- 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/3VVZT46MV6WX4.2U1IN0DNVC2IT%40wilsonb.com.
signature.asc
Description: PGP signature
