Tim Ruffing e78c7b68eb ci/Dockerfile: Reduce size of Docker image further ...

- No need to have wget installed
 - Clean up rm -rf /var/lib/apt/lists/, see
   https://docs.docker.com/develop/develop-images/dockerfile_best-practices/#apt-get

2023-09-03 11:31:35 +02:00

..

ci.sh

ci: Rename cirrus.sh to more general ci.sh

2023-08-18 10:57:58 +01:00

linux-debian.Dockerfile

ci/Dockerfile: Reduce size of Docker image further

2023-09-03 11:31:35 +02:00