lint: upgrade lint scripts for worktrees

Add a ci/lint.py script to run the linter both locally or inside the CI
(replacing .github/ci-lint-exec.py) which supports running from a
worktree.

Determines whether we are in a worktree, and mounts the real `.git`
directory as a read-only volume if we are.
This commit is contained in:
will
2026-01-23 12:09:22 +00:00
parent 1b079becf1
commit c17a2adb8d
4 changed files with 88 additions and 63 deletions

View File

@@ -681,4 +681,6 @@ jobs:
cache-provider: ${{ needs.runners.outputs.provider }}
- name: CI script
run: python .github/ci-lint-exec.py
run: |
git worktree add ../lint-worktree HEAD
../lint-worktree/ci/lint.py