Please add a tag to the last commit of a push to github:public #150
Description
Working on issue #149 I'm trying to find out which patch still works. The problem is that I don't remember which patch was the last one of the last "release", i.e. before the latest rounds of patches where pushed. Unfortunately, randomly choosing a commit does not work very well because at least this far I always ended up with a compilation error at some point. Which is fine because there is no expectation that between any two commits everything should still work. The problem is, without additional information such as a "release tag" added when you push to Github I have no clue what the last working version was that I could test against.
Note that I'm just talking about a git tag, not about a Github "release".