Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit

Permalink
fix(.docker/*): update elan URL (#13928)
Browse files Browse the repository at this point in the history
These are hopefully the last occurrences of the URL that was breaking things earlier today. cf. #13906
  • Loading branch information
bryangingechen committed May 3, 2022
1 parent fd65159 commit 6c0580a
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion .docker/debian/lean/Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ ENTRYPOINT ["/bin/bash", "-l"]
ENV PATH="/home/lean/.elan/bin:/home/lean/.local/bin:$PATH"

# install elan
RUN curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none && \
RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none && \
. ~/.profile && \
elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/leanpkg.toml | grep lean_version | awk -F'"' '{print $2}')
# install leanproject
Expand Down
2 changes: 1 addition & 1 deletion .docker/gitpod/mathlib/Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ WORKDIR /home/gitpod
SHELL ["/bin/bash", "-c"]

# install elan
RUN curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
# install whichever toolchain mathlib is currently using
RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/leanpkg.toml | grep lean_version | awk -F'"' '{print $2}')
# install `leanproject` using `pip`
Expand Down

0 comments on commit 6c0580a

Please sign in to comment.