Abbreviations #1090

	name: Abbreviations

	on:
	schedule:
	- cron: "44 2 * * *"
	workflow_dispatch:

	permissions: {}

	concurrency:
	group: ${{ github.workflow }}

	jobs:
	sync:
	name: Sync abbreviations
	runs-on: ubuntu-latest

	permissions:
	contents: write # for committing updated abbreviation definitions

	steps:
	- uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
	with:
	persist-credentials: true
	- name: Download VSCode abbreviations
	run: \|
	gh api -H 'Accept: application/vnd.github.raw' '/repos/leanprover/vscode-lean4/contents/lean4-unicode-input/src/abbreviations.json' >vscode-lean/abbreviations.json
	env:
	GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
	- name: Commit
	run: \|
	git config user.name "github-actions[bot]"
	git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
	git add -A
	if ! git diff --staged --quiet; then
	git commit -m "Sync abbreviations with the VSCode definitions"
	git push
	fi

Provide feedback