From 3a8aac0d48f4e94e5f3dea13871c02f87938d2ac Mon Sep 17 00:00:00 2001 From: Michael Fliegner <12422482+michaelfliegner@users.noreply.github.com> Date: Fri, 13 Oct 2023 17:43:19 +0200 Subject: [PATCH] Update .gitpod.Dockerfile --- .gitpod.Dockerfile | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/.gitpod.Dockerfile b/.gitpod.Dockerfile index c777707..bfe8c86 100644 --- a/.gitpod.Dockerfile +++ b/.gitpod.Dockerfile @@ -1,14 +1,13 @@ FROM gitpod/workspace-postgres RUN sudo wget https://julialang-s3.julialang.org/bin/linux/x64/1.8/julia-1.8.2-linux-x86_64.tar.gz \ - && tar -xvzf julia-1.8.2-linux-x86_64.tar.gz \ - && ln -s /home/gitpod/julia-1.8.2 julia + && tar -xvzf julia-1.8.2-linux-x86_64.tar.gz # Install direnv RUN sudo apt-get update && sudo apt-get install -y direnv \ && direnv hook bash >> /home/gitpod/.bashrc \ - && echo 'alias runjulia="GENIE_ENV=\"dev\" julia --project=$(pwd)"' >> /home/gitpod/.bashrc \ - && echo 'alias runtest="GENIE_ENV=\"dev\" julia --project=test bootstrap_tests.jl"' >> /home/gitpod/.bashrc \ && mkdir -p .config/direnv \ && echo '[whitelist]' > .config/direnv/config.toml \ - && echo 'prefix = [ "/workspace" ]' >> .config/direnv/config.toml + && echo 'prefix = [ "/workspace", "/home/gitpod"]' >> .config/direnv/config.toml \ + && echo 'PATH_add /home/gitpod/julia-1.8.2/bin' > /home/gitpod/.envrc \ + && echo 'export SEARCHLIGHT_USERNAME="gitpod"' >> /home/gitpod/.envrc