Explicitly set sbatch `--no-requeue` in benchmarking sbatch scripts (… #5386

	name: Docs

	on:
	push:
	tags:
	- 'v[0-9]+.[0-9]+.[0-9]+'
	branches:
	- master
	pull_request:
	branches:
	- master

	jobs:
	doc:
	runs-on: ubuntu-24.04

	steps:
	- name: Install tools
	run: \|
	sudo apt-get update
	sudo apt-get install --no-install-recommends doxygen
	- name: Checkout
	uses: actions/checkout@v4
	- name: Make Docs
	run: \|
	cd doc && make doc && cd ..
	- name: Push Docs master
	if: "github.repository == 'eth-cscs/DLA-Future' && github.ref == 'refs/heads/master'"
	run: \|
	mv doc/html master
	COMMIT_MSG=`git log -n 1 --pretty=format:%s`
	git config user.name "Doc CI Action" && git config user.email "rasolca@users.noreply.github.com"
	git fetch --no-tags --depth=1 origin +refs/heads/docs:refs/heads/docs
	git symbolic-ref HEAD refs/heads/docs && git reset
	git add master && git commit --allow-empty -m "Doc: $COMMIT_MSG" && git push --set-upstream origin docs
	- name: Push Docs release
	if: "github.repository == 'eth-cscs/DLA-Future' && startsWith(github.ref, 'refs/tags/v')"
	run: \|
	TAG=${{ github.ref_name }}
	mv doc/html $TAG
	git config user.name "Doc CI Action" && git config user.email "rasolca@users.noreply.github.com"
	git fetch --no-tags --depth=1 origin +refs/heads/docs:refs/heads/docs
	git symbolic-ref HEAD refs/heads/docs && git reset
	git add $TAG && git commit --allow-empty -m "Doc: add $TAG documentation" && git push --set-upstream origin docs

Provide feedback