This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(measure_theory/order/upper_lower): Order-connected sets in `ℝⁿ` are measurable #7364

	name: Add mathlib4 porting warnings

	on:
	pull_request:

	jobs:
	build:
	name: Check for modifications to ported files
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v3

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

	- name: install latest mathlibtools
	run: \|
	pip install git+https://github.com/leanprover-community/mathlib-tools

	# TODO: is this really faster than just calling git from python?
	- name: Get changed files
	id: changed-files
	uses: Ana06/[email protected]

	- name: run the script
	id: script
	run: \|
	python scripts/detect_ported_files.py ${{ steps.changed-files.outputs.all }}

	- id: PR
	uses: 8BitJonny/[email protected]
	# TODO: this may not work properly if the same commit is pushed to multiple branches:
	# https://github.com/8BitJonny/gh-get-current-pr/issues/8
	with:
	github-token: ${{ secrets.GITHUB_TOKEN }}
	sha: ${{ github.event.pull_request.head.sha }}
	# Only return if PR is still open
	filterOutClosed: true

	- if: steps.script.outputs.modifies_ported == 'True'
	id: add_label
	name: add "modifies-synchronized-file"
	# we use curl rather than octokit/request-action so that the job won't fail
	# (and send an annoying email) if the labels don't exist
	run: \|
	curl -L \
	-X POST \
	-H "Accept: application/vnd.github+json" \
	-H "Authorization: Bearer ${{ secrets.GITHUB_TOKEN }}"\
	-H "X-GitHub-Api-Version: 2022-11-28" \
	https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.PR.outputs.number }}/labels \
	-d '{"labels":["modifies-synchronized-file"]}'

Provide feedback