3.26.0 #12

	name: Auto delete hotfix branch after release
	# We run a scheduled nightly job on hotfix branches (same as master), but we don't need this after
	# doing a release, so delete the branch

	on:
	release:
	types: [published]

	jobs:
	update_benchmark_branches:
	# only run on "hotfix" releases, i.e releases that _don't_ end with .0
	# i.e. run on
	# - 3.2.1
	# - 4.1.2
	# - 3.15.2-prerelease
	# but not on
	# - 3.2.0
	# - 4.1.0
	# - 3.15.0-prerelease
	if: \|
	!endsWith(github.event.release.tag_name, '.0')
	&& !endsWith(github.event.release.tag_name, '.0-prerelease')
	runs-on: ubuntu-latest
	permissions:
	contents: write # Creates and deletes branches
	steps:
	- name: Checkout
	uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
	with:
	fetch-depth: 0

	- uses: actions/setup-dotnet@d4c94342e560b34958eacfc5d055d21461ed1c5d # v5.0.0
	with:
	global-json-file: global.json

	- name: "Output current version"
	id: versions
	run: ./tracer/build.sh OutputCurrentVersionToGitHub

	- name: "Configure Git Credentials"
	run: \|
	git config user.name "${{ github.actor }}"
	git config user.email "${{ github.actor }}@users.noreply.github.com"

	- name: "Delete old hotfix branch"
	run: \|
	hotfix_branch=hotfix/${{ steps.versions.outputs.full_version }}
	git push origin --delete $hotfix_branch;

Provide feedback