vscode: don't round font sizes #41

	# Derived from https://github.com/NixOS/nixpkgs/blob/2ab6f6d61630889491f86396b27a76ffb6fbc7bb/.github/workflows/backport.yml

	name: Backport

	on:
	pull_request_target:
	types: [closed, labeled]

	permissions: {}

	jobs:
	backport:
	name: Backport
	runs-on: ubuntu-latest

	if: >
	(
	github.repository_owner == 'danth' &&
	github.event.pull_request.merged == true &&
	(github.event_name != 'labeled' \|\| startsWith('backport', github.event.label.name))
	)

	steps:
	# Use a GitHub App rather than the default token so that GitHub Actions
	# workflows may run on the created pull request.
	- name: Create GitHub access token
	uses: actions/create-github-app-token@v1
	id: app-token
	with:
	app-id: ${{ vars.BACKPORT_APP_ID }}
	private-key: ${{ secrets.BACKPORT_PRIVATE_KEY }}

	- name: Checkout original pull request
	uses: actions/checkout@v4
	with:
	ref: ${{ github.event.pull_request.head.sha }}
	token: ${{ steps.app-token.outputs.token }}

	- name: Create backport pull request
	uses: korthout/backport-action@v3
	with:
	github_token: ${{ steps.app-token.outputs.token }}
	pull_title: "[${target_branch}] ${pull_title}"
	pull_description: \|-
	This is an automated backport of #${pull_number}.

Provide feedback