File tree Expand file tree Collapse file tree 1 file changed +16
-2
lines changed
developers/docker-ci/latest Expand file tree Collapse file tree 1 file changed +16
-2
lines changed Original file line number Diff line number Diff line change 108
108
ENV HOL4_SMV_EXECUTABLE=/ML/solvers/NuRV
109
109
110
110
# more packages for buliding HOL manuals (+pandoc for Markdown), etc.
111
+ RUN apt-get update
111
112
RUN apt-get install -qy texlive-latex-recommended
112
- RUN apt-get install -qy pandoc latexmk texlive-latex-extra
113
+ RUN apt-get install -qy latexmk texlive-latex-extra
113
114
RUN apt-get install -qy texlive-fonts-extra texlive-science
114
115
RUN apt-get clean
115
116
116
- RUN apt-get clean
117
+ # finally, install a recent pandoc (>= 3.4, with c/line option --table-caption-position=below)
118
+ ARG PANDOC_VERSION="3.7.0.2"
119
+
120
+ RUN if [ "linux/amd64" = "$TARGETPLATFORM" ]; then \
121
+ wget -q https://github.com/jgm/pandoc/releases/download/${PANDOC_VERSION}/pandoc-${PANDOC_VERSION}-1-amd64.deb; \
122
+ dpkg -i pandoc-${PANDOC_VERSION}-1-amd64.deb; \
123
+ rm -f pandoc-${PANDOC_VERSION}-1-amd64.deb; \
124
+ fi
125
+
126
+ RUN if [ "linux/arm64" = "$TARGETPLATFORM" ]; then \
127
+ wget -q https://github.com/jgm/pandoc/releases/download/${PANDOC_VERSION}/pandoc-${PANDOC_VERSION}-1-arm64.deb; \
128
+ dpkg -i pandoc-${PANDOC_VERSION}-1-arm64.deb; \
129
+ rm -f pandoc-${PANDOC_VERSION}-1-arm64.deb; \
130
+ fi
You can’t perform that action at this time.
0 commit comments