File tree Expand file tree Collapse file tree 2 files changed +3
-1
lines changed
.github/actions/build-devcontainer-img Expand file tree Collapse file tree 2 files changed +3
-1
lines changed Original file line number Diff line number Diff line change 70
70
IDRIS_LSP_VERSION=${{ inputs.idris-lsp-version }}
71
71
IDRIS_LSP_SHA=${{ steps.get-sha.outputs.lsp-sha }}
72
72
IDRIS_VERSION=${{ inputs.idris-version }}
73
+ IDRIS_SHA=${{ steps.get-sha.outputs.idris-sha }}
73
74
BASE_IMG=${{ inputs.base-tag }}
74
75
tags : ${{ inputs.tags }}
75
76
load : ${{ inputs.load }}
Original file line number Diff line number Diff line change @@ -9,9 +9,10 @@ ARG BASE_IMG=ghcr.io/joshuanianji/idris-2-docker/base:${IDRIS_VERSION}
9
9
# Rebuild with correct prefix. Somehow, building from scratch with a different prefix fails
10
10
FROM $BASE_IMG as idris-builder
11
11
ARG IDRIS_VERSION
12
+ ARG IDRIS_SHA
12
13
13
14
WORKDIR /build
14
- RUN git clone --depth 1 --branch $IDRIS_VERSION https://github.com/idris-lang/Idris2.git
15
+ RUN git clone https://github.com/idris-lang/Idris2.git && cd Idris2 && git checkout $IDRIS_SHA
15
16
WORKDIR /build/Idris2
16
17
RUN make all PREFIX=/usr/local/lib/idris2
17
18
RUN make install PREFIX=/usr/local/lib/idris2
You can’t perform that action at this time.
0 commit comments