We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent f27676b commit dd32c9dCopy full SHA for dd32c9d
devcontainer-sha.Dockerfile
@@ -9,10 +9,9 @@ ARG BASE_IMG=ghcr.io/joshuanianji/idris-2-docker/base:${IDRIS_VERSION}
9
# Rebuild with correct prefix. Somehow, building from scratch with a different prefix fails
10
FROM $BASE_IMG as idris-builder
11
ARG IDRIS_VERSION
12
-ARG IDRIS_SHA
13
14
WORKDIR /build
15
-RUN git clone https://github.com/idris-lang/Idris2.git && cd Idris2 && git checkout $IDRIS_SHA
+RUN git clone --depth 1 --branch $IDRIS_VERSION https://github.com/idris-lang/Idris2.git
16
WORKDIR /build/Idris2
17
RUN make all PREFIX=/usr/local/lib/idris2
18
RUN make install PREFIX=/usr/local/lib/idris2
0 commit comments