Submitting benchmarks on branch push or on merge commit

**Is your feature request related to a problem? Please describe.**
A push to a branch with an active pull request triggers two events that can be benchmarked:
- push commit: this is a new event on the branch itself, and it is accessible outside the repository with a regular sha,
- test merge commit: this is a github internal test merge commit into the target branch.

We do a fairly standard thing for pipelines with
```
on:
push:
branches:
- main
tags:
- '*'
pull_request:
```
which triggers on the push commit in `main` and for tags only, and triggers on the test merge commit for pull_requests. The GitHub Actions pipelines are therefore run on the test merge commit.

However, the GitLab pipelines that we spin off on eicweb are effectively run on the push commit since we pass (at best) the branch name or push commit sha to eicweb. Technically we should be passing the test merge commit, which we should get with the following:
```console
git fetch origin +refs/pull/${{ github.pull_request.event.number }}/merge
git checkout FETCH_HEAD
```

**Describe the solution you'd like**
This will requires some work on both GitHub and GitLab ends (which we are not doing right now):
- GitHub needs to pass a properly formed ref_name as string
- GitLab needs to clone, fetch the ref, and checkout FETCH_HEAD instead of a simple checkout of sha or branch name

**Describe alternatives you've considered**
Or we could just be happy with running benchmarks on the branch and merging without testing the test merge commit. Together with requiring that pull requests are always up to date with their target branch, this should ensure that the push commit in the branch is the same as the test merge commit. This approach slows down the pace of development since it serializes all benchmarks. We can at most merge at the rate determined by the slowest required benchmark.