File tree Expand file tree Collapse file tree 1 file changed +5
-8
lines changed Expand file tree Collapse file tree 1 file changed +5
-8
lines changed Original file line number Diff line number Diff line change @@ -43,18 +43,15 @@ RUN if [ $IDRIS_VERSION = "latest" ] ; \
43
43
WORKDIR /root/Idris2
44
44
RUN make bootstrap SCHEME=scheme && make install
45
45
46
+ # add idris2 to path
47
+ ENV PATH="/root/.idris2/bin:${PATH}"
48
+ # add idris lib to LD_LIBRARY_PATH
49
+ ENV LD_LIBRARY_PATH="/root/.idris2/lib:${LD_LIBRARY_PATH}"
50
+
46
51
# self-hosting (needed for Idris2 API)
47
52
# in my experience, the Idris2 API seems to still work without the self-hosting step
48
53
# At least, it builds the idris2-python correctly (although i haven't checked anything else)
49
54
# to be safe, I'll do this step anyway
50
55
# NOTE: not sure if the install-api transfers to the child images
51
56
RUN make clean && make all && make install
52
57
RUN make install-api
53
-
54
- # these things aren't strictly necessary for a functioning base image,
55
- # but they make it possible for us to test the image
56
-
57
- # add idris2 to path
58
- ENV PATH="/root/.idris2/bin:${PATH}"
59
- # add idris lib to LD_LIBRARY_PATH
60
- ENV LD_LIBRARY_PATH="/root/.idris2/lib:${LD_LIBRARY_PATH}"
You can’t perform that action at this time.
0 commit comments