Auto merge of #13874 - torhovland:old-syntax-suggestion, r=weihanglo #17

	name: Contrib Deploy
	on:
	push:
	branches:
	- master

	concurrency:
	cancel-in-progress: false
	group: "gh-pages"

	permissions:
	contents: read

	jobs:
	deploy:
	permissions:
	contents: write # for Git to git push
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v4
	with:
	fetch-depth: 0
	- name: Install mdbook
	run: \|
	mkdir mdbook
	curl -Lf https://github.com/rust-lang/mdBook/releases/download/v0.4.37/mdbook-v0.4.37-x86_64-unknown-linux-gnu.tar.gz \| tar -xz --directory=./mdbook
	echo `pwd`/mdbook >> $GITHUB_PATH
	- name: Deploy docs
	run: \|
	GENERATE_PY="$(pwd)/ci/generate.py"

	cd src/doc/contrib
	mdbook build

	# Override previous ref to avoid keeping history.
	git worktree add --orphan -B gh-pages gh-pages
	git config user.name "Deploy from CI"
	git config user.email ""
	cd gh-pages
	mv ../book contrib
	git add contrib

	# Generate HTML for link redirections.
	python3 "$GENERATE_PY"
	git add *.html
	# WARN: The CNAME file is for GitHub to redirect requests to the custom domain.
	# Missing this may entail security hazard and domain takeover.
	# See <https://docs.github.com/en/pages/configuring-a-custom-domain-for-your-github-pages-site/managing-a-custom-domain-for-your-github-pages-site#securing-your-custom-domain>
	git add CNAME

	git commit -m "Deploy $GITHUB_SHA to gh-pages"
	git push origin +gh-pages

Provide feedback