Correctly names the R folder

PRL-PRG · Jan 23, 2025 · 7528e06 · 7528e06
1 parent f57dd0c
commit 7528e06
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile
@@ -72,4 +72,4 @@ RUN curl -fsSL -o /opt/llvm.sh https://apt.llvm.org/llvm.sh \
 # Install R
 COPY ./build-gnur-in-docker.sh /workspace/tools/build-gnur-in-docker.sh
 RUN mkdir -p /workspace/external/R
-RUN cd /workspace/external ; bash ../tools/build-gnur-in-docker.sh R
+#RUN cd /workspace/external ; bash ../tools/build-gnur-in-docker.sh R
diff --git a/.devcontainer/build-gnur-in-docker.sh b/.devcontainer/build-gnur-in-docker.sh
@@ -59,6 +59,7 @@ if [[ ! -f ${R_DIR}/.git ]]; then
   # of the  script is used when building the Docker image
   echo "-> fetch modified R sources"
   git clone https://github.com/PRL-PRG/r-compiler-server-gnur
+  rm -rf "$R_DIR"
   mv r-compiler-server-gnur "$R_DIR"
 fi