Repository navigation

Fail CI when regenerated sources differ from the committed ones - #3

Merged

MisterGC merged 2 commits into

Oct 7, 2026

Commits on Oct 5, 2026
- Always regenerate sources in CI by ignoring timestamps
  MisterGC
  committed
  02171d7
- Fail sources regeneration on a non-empty git diff
  MisterGC
  committed
  2053e60