Rename CI pipeline to try to eliminate some caching issue on git/ci host

This commit is contained in:
vanous 2022-07-21 08:13:32 +02:00
parent 1dd22da1b2
commit e1ced2e80b