Properly recognize whether the current commit is a tag (#7989)
authorGereon Kremer <gkremer@stanford.edu>
Thu, 27 Jan 2022 00:34:16 +0000 (16:34 -0800)
committerGitHub <noreply@github.com>
Thu, 27 Jan 2022 00:34:16 +0000 (00:34 +0000)
commit47d619f8600c8c409ce8849dcbddc72fa314371b
tree113b00f00002fa07bc50803a935da5bde490eb77
parent8e42644dd87d217b98ec88207c2c7f30ef54261a
Properly recognize whether the current commit is a tag (#7989)

This actually fixes what #7901 tried: when uploading the documentation, we need to figure out whether it was a tag and we should upload as a release as well.
Furthermore it fixes how we setup the deploy keys.
.github/workflows/docs_upload.yml