Repository navigation

Pass CI for pull requests whose changes are already on main - #138

Merged

woksin merged 1 commit into

mainfrom

fix/109-no-changed-files

Sep 29, 2026

Commits on Sep 29, 2026
- Treat a pull request with no changed files as nothing to check
  woksin
  committed
  4e73e9e