.github/with-docker/Dockerfile: add curl command

runtimeverification · Sep 4, 2024 · c5e1ba2 · c5e1ba2
1 parent 8994591
commit c5e1ba2
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/.github/actions/with-docker/Dockerfile b/.github/actions/with-docker/Dockerfile
@@ -13,6 +13,7 @@ ARG PYTHON_VERSION=3.10
 
 RUN    apt-get -y update             \
     && apt-get -y install            \
+         curl                        \
          graphviz                    \
          python${PYTHON_VERSION}     \
          python${PYTHON_VERSION}-dev \