Exclude dir - #4

Merged

samuelburnham merged 10 commits into

devfrom

Sep 2, 2026

Commits on Aug 27, 2026

feat: Exclude a directory from a package directory glob
samuelburnham
committed
265fcda
Update flake.lock
samuelburnham
committed
8075eb8

Commits on Aug 28, 2026

ci: Restrict the E2E workflow to a read-only token
samuelburnham
committed
448b22a
ci: Restrict the CI and test workflows to a read-only token
samuelburnham
committed
5951955
ci: Open the self-update PR with GITHUB_TOKEN
samuelburnham
committed
aece5d9

Commits on Sep 1, 2026

docs: Record what the default token cannot do
samuelburnham
committed
ac315a0
fix: Reject a bare `!` package directory exclusion
samuelburnham
committed
50d4c61
ci: Silence the failure outcome in the test workflow
samuelburnham
committed
fe7af4b
fix: Get the Mathlib cache for every target package
samuelburnham
committed
b0ed23f
feat: Fail validation when a required Mathlib cache is missing
samuelburnham
committed
728a375