internal/ci: delete completed TODO about the old registry tokens #895

	# Code generated internal/ci/ci_tool.cue; DO NOT EDIT.

	name: Push tip to trybot
	"on":
	push:
	branches:
	- master
	- release-branch.*
	concurrency: push_tip_to_trybot
	jobs:
	push:
	runs-on: ubuntu-24.04
	steps:
	- name: Write netrc file for cueckoo Gerrithub
	run: \|-
	cat <<EOD > ~/.netrc
	machine review.gerrithub.io
	login cueckoo
	password ${{ secrets.CUECKOO_GERRITHUB_PASSWORD }}
	EOD
	chmod 600 ~/.netrc
	- name: Push tip to trybot
	run: \|-
	mkdir tmpgit
	cd tmpgit
	git init -b initialbranch
	git config user.name cueckoo
	git config user.email [email protected]
	git config http.https://github.com/.extraheader "AUTHORIZATION: basic $(echo -n cueckoo:${{ secrets.CUECKOO_GITHUB_PAT }} \| base64)"
	git remote add origin https://review.gerrithub.io/a/cue-lang/cue
	git remote add trybot https://github.com/cue-lang/cue-trybot

	git fetch origin "${{ github.ref }}"

	success=false
	for try in {1..20}; do
	echo "Push to trybot try $try"
	if git push -f trybot "FETCH_HEAD:${{ github.ref }}"; then
	success=true
	break
	fi
	sleep 1
	done
	if ! $success; then
	echo "Giving up"
	exit 1
	fi
	defaults:
	run:
	shell: bash
	if: ${{github.repository == 'cue-lang/cue'}}

Provide feedback