fix: save extensions in workdir

SwissDataScienceCenter · Nov 23, 2024 · e9b3a57 · e9b3a57
1 parent 9f5ab87
commit e9b3a57
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 2 deletions.
diff --git a/docker/vscode/base.Dockerfile b/docker/vscode/base.Dockerfile
@@ -11,6 +11,8 @@ RUN apt-get update && \
 	rm -rf /var/lib/apt/lists/*
 
 USER ${SESSION_USER}
+COPY entrypoint.sh /entrypoint.sh
 WORKDIR ${WORKDIR}
-ENTRYPOINT ["tini", "--", "sh", "-c"]
-CMD ["/codium-server/bin/codium-server --server-base-path $RENKU_BASE_URL_PATH/ --without-connection-token --host 0.0.0.0 --port 8888"]
+# We are setting this to a weird double underscore name to avoid collisions with user-set vars
+ENV __WORKDIR__=${WORKDIR}
+ENTRYPOINT ["tini", "--", "/bin/bash", "/entrypoint.sh"]
diff --git a/docker/vscode/entrypoint.sh b/docker/vscode/entrypoint.sh
@@ -0,0 +1,12 @@
+set -ex
+WORKDIR=${__WORKDIR__}
+mkdir -p "${WORKDIR}/.vscode/extensions"
+/codium-server/bin/codium-server \
+	--server-base-path "$RENKU_BASE_URL_PATH/" \
+	--without-connection-token \
+	--host 0.0.0.0 \
+	--port 8888 \
+	--extensions-dir "${WORKDIR}/.vscode/extensions" \
+	--accept-server-license-terms \
+	--telemetry-level off \
+	--server-data-dir "${WORKDIR}/.vscode"