From ea7165bbc268ead7c8f3eed77a6555186d15bbcf Mon Sep 17 00:00:00 2001 From: Sascha Lisson Date: Sat, 2 Nov 2024 10:24:25 +0100 Subject: [PATCH] install wget --- src/mps/install.sh | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/mps/install.sh b/src/mps/install.sh index d3cab14..a74f6d0 100644 --- a/src/mps/install.sh +++ b/src/mps/install.sh @@ -24,7 +24,8 @@ echo "The effective dev container containerUser's home directory is '$_CONTAINER # install packages ( apt-get update -y - apt-get -y install --no-install-recommends wget + apt-get -y install --no-install-recommends wget ca-certificates + update-ca-certificates mkdir /tmp/mps cd /tmp/mps wget "https://download.jetbrains.com/mps/${MPS_MAJOR_VERSION}/MPS-${MPS_VERSION}.tar.gz"