Tobias Brunner 8468b43891 github: Prevent duplicate CI runs ... This cancels previous runs of the same branch and skips runs of the same content (e.g. after merges or tags).		2020-12-15 10:42:43 +01:00
..
actions/default	github: Migrate from Travis CI to Github Actions	2020-12-15 10:42:43 +01:00
workflows	github: Prevent duplicate CI runs	2020-12-15 10:42:43 +01:00