Alexander Wilms 5222495701 Run CI on every push to develop branch instead of on a schedule ... Also remove logic to skip CI if it already ran for the same commit This prevents the CI badge in the README from showing a failure due to a skipped CI run and results in more up-to-date ccache caches for each PR's initial CI run		2024-01-30 20:51:27 +01:00
..
github.yml	Run CI on every push to develop branch instead of on a schedule	2024-01-30 20:51:27 +01:00