Tim Ruffing 98579e297b ci: Drop manual checkout of merge commit ...

This is no longer necessary as of
https://github.com/cirruslabs/cirrus-ci-docs/issues/791#issuecomment-1615691585 .

2023-07-01 13:01:57 +02:00

..

cirrus.sh

ci: Drop manual checkout of merge commit

2023-07-01 13:01:57 +02:00

linux-debian.Dockerfile

ci: Adjust Docker image to Debian 12 "bookworm"

2023-06-26 10:24:15 +01:00