Repository navigation

improvement(workspaces): move workspace updates behind an application operation and let Chat rename workspaces #24

	name: cache cleanup

	on:
	pull_request:
	types: [closed]

	permissions:
	contents: read

	concurrency:
	group: cache-cleanup-${{ github.event.pull_request.number }}
	cancel-in-progress: false

	jobs:
	cleanup:
	if: >-
	github.event.pull_request.head.repo.full_name == github.repository
	&& github.event.pull_request.user.login != 'dependabot[bot]'
	&& github.actor != 'dependabot[bot]'
	runs-on: ubuntu-24.04
	timeout-minutes: 5
	permissions:
	actions: write
	pull-requests: read
	steps:
	- name: Remove caches scoped to the closed pull request
	env:
	GH_TOKEN: ${{ github.token }}
	GH_REPO: ${{ github.repository }}
	PR_NUMBER: ${{ github.event.pull_request.number }}
	run: \|
	state=$(gh pr view "$PR_NUMBER" --json state --jq .state)
	case "$state" in
	OPEN) exit 0 ;;
	CLOSED\|MERGED) ;;
	*) echo "::error::Unexpected pull request state: $state"; exit 1 ;;
	esac
	gh cache delete --all --ref "refs/pull/${PR_NUMBER}/merge" --succeed-on-no-caches