Add Dev Container Configuration Files (#7)

This commit is contained in:
Olivier Benz
2023-07-23 17:35:21 +02:00
committed by GitHub
parent 4f7ab0ac1b
commit 931b138bb1
21 changed files with 441 additions and 0 deletions

View File

@@ -0,0 +1,17 @@
#!/usr/bin/env bash
# Copyright (c) 2023 b-data GmbH.
# Distributed under the terms of the MIT License.
set -e
mkdir -p "${HOME}/.julia/config"
# Copy user-specific startup files if home directory is bind mounted
if [ ! -f "${HOME}/.julia/config/startup_ijulia.jl" ]; then
cp -a /etc/skel/.julia/config/startup_ijulia.jl \
"${HOME}/.julia/config"
fi
if [ ! -f "${HOME}/.julia/config/startup.jl" ]; then
cp -a /etc/skel/.julia/config/startup.jl \
"${HOME}/.julia/config"
fi