Merge pull request #82 from johnnychen94/jc/julia

[Julia] make /opt/julia a shared julia depot path
This commit is contained in:
Yuxiang Zhang 2020-08-09 21:20:14 +08:00 committed by GitHub
commit 1589b2e8d9
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 12 additions and 2 deletions

View File

@ -4,11 +4,16 @@
# StorageServer.jl is used to set up a *static* storage server for julia packages, it requires at least Julia 1.4 # StorageServer.jl is used to set up a *static* storage server for julia packages, it requires at least Julia 1.4
# The details of the storage protocol can be found in https://github.com/JuliaLang/Pkg.jl/issues/1377 # The details of the storage protocol can be found in https://github.com/JuliaLang/Pkg.jl/issues/1377
FROM julia:1.4 FROM julia:1.5
LABEL description="A community maintained docker script to set up julia mirror easily." LABEL description="A community maintained docker script to set up julia mirror easily."
LABEL maintainer="Johnny Chen <johnnychen94@hotmail.com>" LABEL maintainer="Johnny Chen <johnnychen94@hotmail.com>"
RUN julia -e 'using Pkg; pkg"add https://github.com/johnnychen94/StorageMirrorServer.jl#v0.1.1-rc3"' ENV JULIA_DEPOT_PATH="/opt/julia"
RUN julia -e 'using Pkg; pkg"add https://github.com/johnnychen94/StorageMirrorServer.jl#v0.1.1-rc3"' && \
chmod a+rx -R $JULIA_DEPOT_PATH
COPY startup.jl /usr/local/julia/etc/julia/startup.jl
WORKDIR /julia WORKDIR /julia
CMD /bin/bash CMD /bin/bash

View File

@ -0,0 +1,5 @@
SHARE_DIR = "/opt/julia"
empty!(DEPOT_PATH)
push!(DEPOT_PATH, joinpath(homedir(), ".julia"), SHARE_DIR)
push!(LOAD_PATH, SHARE_DIR)