fix(naming): rename option to skip merge files #1983

	name: Performance benchmark

	on:
	pull_request:
	workflow_dispatch:
	inputs:
	run_options:
	description: 'Additional options to pass to `run`'
	python_version:
	description: 'Python version to use (use https://github.com/actions/setup-python#supported-version-syntax)'
	default: '3.10'

	jobs:
	benchmark:
	name: Run performance benchmark
	if: ${{ !github.event.pull_request.head.repo.fork }}
	runs-on: ubuntu-22.04
	env:
	PYTHONUNBUFFERED: 1
	# How many time to repeat each run
	REPEATS: 3
	# If a run takes more than $MAX_DELTA seconds compared to reference, fail the job
	MAX_DELTA: 3
	steps:
	- name: Check out the repo
	uses: actions/checkout@v4
	with:
	fetch-depth: 0

	- name: Set up Python
	uses: actions/setup-python@v4
	with:
	python-version: ${{ inputs.python_version \|\| '3.10' }}

	- name: Install dependencies
	run: \|
	python --version
	python -m pip install --upgrade pip
	python -m pip install pipenv==2023.12.1
	pipenv install --system --skip-lock

	- name: Setup benchmark
	run: \|
	scripts/perfbench/perfbench setup

	- name: Run benchmark
	env:
	GITGUARDIAN_API_KEY: ${{ secrets.GITGUARDIAN_API_KEY }}
	run: \|
	scripts/perfbench/perfbench run --repeats $REPEATS ${{ inputs.run_options }}

	- name: Generate report
	run: \|
	scripts/perfbench/perfbench report --max-delta $MAX_DELTA >> $GITHUB_STEP_SUMMARY

Provide feedback