Files
0ad/.gitea
Ralph Sennhauser 2ed912ae88 Disable push trigger for lint workflow
The event property github.event.push.before seems to not be supported
and therefore the workflow as is fails on main.

Ignoring the trigger means a slight loss in coverage but as it still
fully checks PRs we are mostly good.

Signed-off-by: Ralph Sennhauser <ralph.sennhauser@gmail.com>
2025-03-31 20:23:41 +02:00
..