Azure Pipelines has direct integration with GitHub, so we're just using
that. Releases on GitHub have to target a tag, so we also need to push
the tag as an intermediate step; we also need to include the platform
name in the artifact to avoid overwriting from different builds.
The two "GitHub release" steps depend on two Azure variables that are
not defined in the pipeline script. This may look like it should not
work, but in fact it does, because these variables are set by the
release script.
In Azure Pipelines, any build step can set variables for the next build
steps by outputting specially-formatted text to stdout. This text will
not appear in the build output displayed by Azure Pipelines, e.g.:
```
echo '##vso[task.setvariable variable=sauce]tomatoes'
```
would define the Azure variable `sauce` to have the string `tomatoes` as
its value for the next build steps.
See [0] for details.
[0]: https://docs.microsoft.com/en-us/azure/devops/pipelines/process/variables?view=azure-devops&tabs=yaml%2Cbatch#set-in-script