Supporting monorepos like homalg_project

[zickgraf]

homalg_project uses a modified version of the release tools to support monorepos. I have rebased these modifications on the current master and would like to discuss if/how I could upstream the changes in zickgraf@0516577

1. The --update-file flag, cd "$SRC_DIR", rm -rf .github .circleci, and maybe git add -A could be taken as is, I assume.
2. If $TAG is not the HEAD commit, we do not want to display an error, as this case is expected for mono-repos (as not all packages of the mono-repo are released from the same commit). Maybe we could put the desired behaviour behind a flag like --no-old-tag-error? (Suggestions for better names are welcome :D ) superseded by point 4.
3. The name of the release should include the package name to distinguish releases of different packages. I see the following possibilities:
   1. Reuse the tag name as the release name (would change existing behaviour).
   2. Use "$PKG-$VERSION" or "$PKG $VERSION" as the release name (would change existing behaviour)
   3. Keep "$VERSION" as the release name but allow to pass a prefix via a new argument --release-name-prefix.
4. We always run the release script on all packages in the repository, so there is a high chance that a package already has a current release. Thus, I have moved the check if a GitHub release already exists to the beginning, and have added a flag --skip-existing-release to simply skip the release and return without error in that case.
5. For git push "$REMOTE" I have already opened a PR.

cc @mohamed-barakat

[fingolfin]

Re 1: just go ahead and submit a PR, we can discuss details there, if necessary

Re 3: what exactly do you mean with "name of the release"? The stem of the filename used for the archives? I can't really comment until I understand what this is about

Re 4: I don't mind adding such an option, as long as it is off by default, because the current behavior is intentionally there to catch a (sadly) not uncommon class of user mistake (namely forgetting to increment the version / trying to reuse a version which should be done only if one really really knows what one is doing).

Re 5.: that was taken care of by PR #71, right?

[zickgraf]

Re 1: Done, see #77 :-)

Re 3: I mean this line: zickgraf@0516577#diff-534e5230fcedccac15ecdc0c8f6a9f280dd2f762499d90e85ee34c24834c11acR546 That is, the "title" of the release when shown on GitHub.

Re 4: Done in #77, off by default.

Re 5: Correct!

[fingolfin]

Re 3: aaah ok, now I get it. Is this used for anything other than letting users read it? Then I'd go for "$PKG $VERSION" without a dash.

[zickgraf]

Re 3: aaah ok, now I get it. Is this used for anything other than letting users read it?

I just checked and it really seems to only be used for humans: the link to the release and the API both rely on the tag name. I have just pushed the change to the existing PR, so everything should be handled now :-)

[zickgraf]

Fixed by PR #77.