Release tags wrong commit

[polothy]

We recently had two PRs merge and the same time. The one that merged first, ended up tagging the commit of the 2nd. Then the 2nd cancelled itself because the commit was already tagged.

In the release_github job, it has this step to make the tag:

      - name: Release
        env:
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
          GITHUB_REPOSITORY: ${{ github.repository }}
          GITHUB_REF: ${{ github.ref }}
        run: errout=$(mktemp); gh release create $(cat dist/releasetag.txt) -R $GITHUB_REPOSITORY -F dist/changelog.md -t $(cat dist/releasetag.txt) --target $GITHUB_REF 2> $errout && true; exitcode=$?; if [ $exitcode -ne 0 ] && ! grep -q "Release.tag_name already exists" $errout; then cat $errout; exit $exitcode; fi

The problem, I think, is that GITHUB_REF: ${{ github.ref }} should be GITHUB_REF: ${{ github.sha }}. The ref changed during the release, so it ended up tagging the wrong commit.

[polothy]

Lame attempt: #3584 - at the very least, shows where to fix the problem I think.