ci: drop push:dev trigger; PR is the gate #25

Merged
bvandeusen merged 262 commits from dev into main 2026-04-28 08:35:54 -04:00
Showing only changes of commit a52fdc7d5d - Show all commits