Explain Firefox how numeric input should work #3121

	# Github UI does not support merges that preserve the commit revision of the PR
	# branch (fast forward merging).
	#
	# See also this issue: https://github.com/community/community/discussions/4618
	#
	# Since we store benchmark results from PRs with the revision information from
	# the PR branch, ideally we'd like to preserve the results that we stored for a
	# given revision while developing on the feature branch and still be able to
	# lookup results on a commit id once it lands in main. If the commit IDs change
	# that makes it harder.
	#
	# Hence this script allows to do a fast-forward merge by commenting
	# /fast-forward on the PR. With /fast-forward the commit IDs are preserved
	# between the feature branch and the main branch.
	name: Fast-forward

	on:
	issue_comment:
	types: [created, edited]

	jobs:
	fast_forward:
	name: Fast-forward
	runs-on: [self-hosted, Linux, skylake-2x]
	if: \|
	github.event.issue.pull_request &&
	contains(github.event.comment.body, '/fast-forward')

	steps:

	- name: Fetch repository
	uses: actions/checkout@v3
	with:
	fetch-depth: 0

	- name: Checkout pull request
	run: hub pr checkout ${{ github.event.issue.number }}
	env:
	GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

	- name: Fast-forward & push
	run: \|
	export PR_COMMIT=$(git rev-parse HEAD)
	git checkout main
	git merge --ff-only "$PR_COMMIT"
	git push origin main

Provide feedback