Merge remote-tracking branch 'origin/v21' into bidi-page-goback-forward #1820

	name: on-push-do-docs
	on:
	push:
	jobs:
	docs:
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v2
	- name: Setup .NET
	uses: actions/setup-dotnet@v3
	with:
	dotnet-version: 7.0.x
	- name: Run MarkdownSnippets
	run: \|
	dotnet tool install --global MarkdownSnippets.Tool
	mdsnippets ${GITHUB_WORKSPACE}
	shell: bash
	- name: Push changes
	run: \|
	git config --local user.email "[email protected]"
	git config --local user.name "GitHub Action"
	git commit -m "Docs changes" -a \|\| echo "nothing to commit"
	remote="https://${GITHUB_ACTOR}:${{secrets.GITHUB_TOKEN}}@github.com/${GITHUB_REPOSITORY}.git"
	branch="${GITHUB_REF:11}"
	git push "${remote}" ${branch} \|\| echo "nothing to push"
	shell: bash

Provide feedback