fix: ignore Aesop tactic/commands in unused tactics linter #45398

	name: Label New Contributors

	# Written with ChatGPT: https://chat.openai.com/share/3777ceb1-d722-4705-bacd-ba3f04b387be

	on: pull_request

	jobs:
	label-and-report-new-contributor:
	runs-on: ubuntu-latest
	# Don't run on forks, where we wouldn't have permissions to add the label anyway.
	if: github.repository == 'leanprover-community/mathlib4'
	permissions:
	checks: write
	pull-requests: write
	contents: read
	steps:
	- name: Label PR and report count
	uses: actions/github-script@v7
	with:
	script: \|
	const creator = context.payload.sender.login
	const { owner, repo } = context.repo;
	const opts = github.rest.issues.listForRepo.endpoint.merge({
	...context.issue,
	owner,
	repo,
	creator,
	state: 'closed'
	})
	const issues = await github.paginate(opts)
	const pullRequestCount = issues.length;

	// Determine if the creator has 5 or fewer pull requests
	if (pullRequestCount <= 5) {
	// Add the "new-contributor" label to the current pull request
	await github.rest.issues.addLabels({
	issue_number: context.issue.number,
	owner,
	repo,
	labels: ['new-contributor']
	});
	}

	// Create a check run with a message about the PR count by this author
	const message = `Found ${pullRequestCount} PRs by ${creator}.`;
	await github.rest.checks.create({
	owner,
	repo,
	name: 'New Contributor Check',
	head_sha: context.payload.pull_request.head.sha,
	status: 'completed',
	conclusion: 'neutral',
	output: {
	title: message,
	summary: message,
	},
	});

Provide feedback