use curl instead of wget

modelix · Nov 2, 2024 · aa1bfa1 · aa1bfa1
1 parent c7c9de2
commit aa1bfa1
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/src/mps/devcontainer-feature.json b/src/mps/devcontainer-feature.json
@@ -1,5 +1,5 @@
 {
-    "name": "Hello, World!",
+    "name": "JetBrains MPS",
     "id": "mps",
     "version": "1.0.0",
     "description": "Installs JetBrains MPS",

diff --git a/src/mps/install.sh b/src/mps/install.sh
@@ -25,8 +25,8 @@ echo "The effective dev container containerUser's home directory is '$_CONTAINER
 (
   mkdir /tmp/mps
   cd /tmp/mps
-  wget "https://download.jetbrains.com/mps/${MPS_MAJOR_VERSION}/MPS-${MPS_VERSION}.tar.gz"
-  tar -xf $(ls | head -n 1)
+  curl -o mps.tar.gz "https://download.jetbrains.com/mps/${MPS_MAJOR_VERSION}/MPS-${MPS_VERSION}.tar.gz"
+  tar -xf mps.tar.gz
   mv "MPS $MPS_MAJOR_VERSION" "/mps"
 )