CI: Assign milestone on merged PRs (#4414) #12713

	---
	name: General linting

	on:
	push:
	branches:
	- main
	- releasebranch_*
	pull_request:

	concurrency:
	group: ${{ github.workflow }}-${{ github.event_name == 'pull_request' && github.head_ref \|\| github.sha }}
	cancel-in-progress: true

	jobs:
	super-linter:
	name: GitHub Super Linter

	runs-on: ubuntu-latest

	permissions:
	contents: read
	packages: read
	# To report GitHub Actions status checks
	statuses: write

	steps:
	- uses: actions/checkout@692973e3d937129bcbf40652eb9f2f61becf3332 # v4.1.7
	with:
	# super-linter needs the full git history to get the
	# list of files that changed across commits
	fetch-depth: 0
	- name: Lint code base
	uses: super-linter/super-linter/slim@88ea3923a7e1f89dd485d079f6eb5f5e8f937589 # v6.6.0
	env:
	DEFAULT_BRANCH: main
	# To report GitHub Actions status checks
	GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
	# Listed but commented out linters would be nice to have.
	# (see https://github.com/github/super-linter#environment-variables)
	#
	# Python (supported using Pylint) and C/C++ (not supported) are
	# handled separately due to the complexity of the settings.
	# VALIDATE_BASH: true
	VALIDATE_BASH_EXEC: true
	# VALIDATE_CSS: true
	# VALIDATE_DOCKER: true
	VALIDATE_JAVASCRIPT_ES: true
	# VALIDATE_JAVASCRIPT_STANDARD: true
	VALIDATE_JSON: true
	VALIDATE_MARKDOWN: true
	VALIDATE_POWERSHELL: true
	# VALIDATE_XML: true
	VALIDATE_YAML: true

Provide feedback