[Merged by Bors] - refactor(Measure): replace `trimmed` with `trim_le` #53683

	name: Detect changes to header SHAs

	on:
	pull_request:

	jobs:
	build:
	name: Add annotations
	runs-on: ubuntu-latest
	env:
	GH_TOKEN: ${{ github.token }}
	steps:
	- name: "Checkout mathlib4"
	uses: actions/checkout@v4

	- name: "Checkout mathlib3"
	uses: actions/checkout@v4
	with:
	repository: leanprover-community/mathlib
	path: port-repos/leanprover-community/mathlib

	- name: "Checkout lean3"
	uses: actions/checkout@v4
	with:
	repository: leanprover-community/lean
	path: port-repos/leanprover-community/lean

	- name: Fetch merge base SHA from API
	run: \|
	my_merge_base_cmd="gh api repos/${{ github.repository }}/compare/${{ github.event.pull_request.base.sha }}...${{ github.event.pull_request.head.sha }} \| jq -r '.merge_base_commit.sha'"
	echo "${my_merge_base_cmd}"
	my_merge_base="$(eval "${my_merge_base_cmd}")"
	printf 'MY_MERGE_BASE_SHA=%s\n' "${my_merge_base}" >> "${GITHUB_ENV}"

	- name: Fetch merge base SHA
	run: \|
	git fetch \
	--no-tags \
	--prune \
	--progress \
	--no-recurse-submodules \
	--depth=1 \
	origin "${MY_MERGE_BASE_SHA}"

	- name: install Python
	uses: actions/setup-python@v4
	with:
	python-version: 3.8

	- name: install script dependencies
	run: \|
	pip install gitpython

	- name: run the script
	run: \|
	python scripts/detect_sha_changes.py "${MY_MERGE_BASE_SHA}" "HEAD"

Provide feedback