File tree 2 files changed +0
-25
lines changed
2 files changed +0
-25
lines changed Original file line number Diff line number Diff line change @@ -13,29 +13,8 @@ WORKDIR /home/gitpod
13
13
14
14
SHELL ["/bin/bash" , "-c" ]
15
15
16
- # # gitpod bash prompt
17
- # RUN { echo && echo "PS1='\[\033[01;32m\]\u\[\033[00m\] \[\033[01;34m\]\w\[\033[00m\]\$(__git_ps1 \" (%s)\") $ '" ; } >> .bashrc
18
-
19
16
# install elan
20
17
RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
21
18
22
19
ENV PATH="/home/gitpod/.local/bin:/home/gitpod/.elan/bin:${PATH}"
23
20
24
- # WORKDIR /workspace/PrimeNumberTheoremAnd
25
- #
26
- # RUN . ~/.profile
27
- #
28
- # RUN elan toolchain install $(cat /workspace/PrimeNumberTheoremAnd/lean-toolchain)
29
- #
30
- # RUN lake exe cache get
31
- # RUN lake build
32
-
33
- # # fix the infoview when the container is used on gitpod:
34
- # ENV VSCODE_API_VERSION="1.50.0"
35
-
36
- # # ssh to github once to bypass the unknown fingerprint warning
37
- # RUN ssh -o StrictHostKeyChecking=no github.com || true
38
- #
39
- # # run sudo once to suppress usage info
40
- # RUN sudo echo finished
41
-
Original file line number Diff line number Diff line change 14
14
15
15
command: lake build
16
16
17
-
18
-
19
- # - command: . /home/gitpod/.profile && lake exe cache get # Download cache
20
-
You can’t perform that action at this time.
0 commit comments