File tree 1 file changed +2
-1
lines changed
1 file changed +2
-1
lines changed Original file line number Diff line number Diff line change @@ -40,7 +40,7 @@ RUN wget https://github.com/MLton/mlton/releases/download/on-20210117-release/ml
40
40
# It is supposed to have the effect of re-cloning this repository
41
41
# (i.e. invalidating the docker cache at this layer) if and only if
42
42
# the branch actually changes.
43
- ADD https://api.github.com/repos/agoode/mlton/git/refs/heads/wasm2 version.json
43
+ ADD https://api.github.com/repos/agoode/mlton/git/refs/heads/wasm2 mlton- version.json
44
44
RUN git clone -b wasm2 https://github.com/agoode/mlton mlton
45
45
46
46
# build mlton binary
@@ -67,6 +67,7 @@ RUN echo '#!/bin/bash\ngit rev-parse HEAD' > /usr/bin/svnversion && \
67
67
chmod +x /usr/bin/svnversion
68
68
69
69
# build twelf binary in $BUILD/twelf/bin/twelf.wasm
70
+ ADD https://api.github.com/repos/standardml/twelf/git/refs/heads/main twelf-version.json
70
71
RUN git clone https://github.com/standardml/twelf && \
71
72
cd twelf && \
72
73
make mlton="$BUILD/mlton-INSTALL/bin/mlton \
You can’t perform that action at this time.
0 commit comments