From 39d8e2926d347449d5dfd0e64c3044eeeaac28d1 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 20 Sep 2024 18:48:13 -0700 Subject: [PATCH] Install python-is-python3 in github-actions-docker-make.sh --- etc/ci/github-actions-docker-make.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/etc/ci/github-actions-docker-make.sh b/etc/ci/github-actions-docker-make.sh index 92b41e9b6c..dcd7659cc1 100755 --- a/etc/ci/github-actions-docker-make.sh +++ b/etc/ci/github-actions-docker-make.sh @@ -14,7 +14,7 @@ sudo chmod -R a=u . git config --global --add safe.directory "*" echo '::group::install general dependencies' sudo apt-get update -y -sudo apt-get install -y python python3 bsdmainutils ${EXTRA_PACKAGES} +sudo apt-get install -y python-is-python3 python3 bsdmainutils ${EXTRA_PACKAGES} eval $(opam env) echo '::endgroup::' echo '::remove-matcher owner=coq-problem-matcher::'