File tree Expand file tree Collapse file tree 2 files changed +0
-6
lines changed Expand file tree Collapse file tree 2 files changed +0
-6
lines changed Original file line number Diff line number Diff line change @@ -28,7 +28,6 @@ RUN apt-get update && \
28
28
apt-get install -y git make gcc libgmp-dev curl
29
29
30
30
ENV DEBIAN_FRONTEND noninteractive
31
- ARG IDRIS_VERSION
32
31
# SHA of the latest commit on the idris-lang/idris2 repo
33
32
ARG IDRIS_SHA
34
33
@@ -38,8 +37,6 @@ COPY --from=scheme-builder /root/scheme-lib/ /usr/lib/
38
37
COPY --from=scheme-builder /root/scheme-lib/ /root/scheme-lib
39
38
40
39
WORKDIR /root
41
- # if IDRIS_VERSION is 'latest', do not switch to a branch. Checkout the latest commit - ensures docker cache won't use stale versions
42
- # https://stackoverflow.com/a/41361804
43
40
RUN git clone https://github.com/idris-lang/Idris2.git && cd Idris2 && git checkout $IDRIS_SHA
44
41
WORKDIR /root/Idris2
45
42
RUN make bootstrap SCHEME=scheme && make install
@@ -58,5 +55,4 @@ RUN make clean && make all && make install
58
55
RUN make install-api
59
56
60
57
# re-expose version information
61
- ENV IDRIS_VERSION=$IDRIS_VERSION
62
58
ENV IDRIS_SHA=$IDRIS_SHA
Original file line number Diff line number Diff line change @@ -54,7 +54,6 @@ FROM mcr.microsoft.com/vscode/devcontainers/base:bullseye
54
54
55
55
ARG IDRIS_LSP_VERSION=latest
56
56
ARG IDRIS_LSP_SHA
57
- ARG IDRIS_VERSION
58
57
ARG IDRIS_SHA
59
58
60
59
# idris2 + idris2-lsp compiled from source
@@ -72,6 +71,5 @@ ENV SCHEME=scheme
72
71
# re-expose version information
73
72
ENV IDRIS_LSP_VERSION=$IDRIS_LSP_VERSION
74
73
ENV IDRIS_LSP_SHA=$IDRIS_LSP_SHA
75
- ENV IDRIS_VERSION=$IDRIS_VERSION
76
74
ENV IDRIS_SHA=$IDRIS_SHA
77
75
You can’t perform that action at this time.
0 commit comments