Repository navigation

Reuse unchanged PR builds during ordinary CI - #605

Merged

Vilin97 merged 3 commits into

mainfrom

codex/ci-pr-build-reuse

Oct 7, 2026

Merged

Reuse unchanged PR builds during ordinary CI#605
Vilin97 merged 3 commits into
mainfrom
codex/ci-pr-build-reuse

Commits on Oct 6, 2026
- Reuse unchanged PR builds before ordinary CI compilation
  Vilin97
  committed
  2e981ba
- Harden artifact restoration and run dependency checks with pinned Lean
  Vilin97
  committed
  15dcc57
Commits on Oct 7, 2026
- Merge remote-tracking branch 'origin/main' into codex/ci-pr-build-reuse
  Vilin97
  committed
  5b6b848