Fixed building HOL manuals with PolyML (and not in --otknl)

HOL-Theorem-Prover · May 3, 2024 · 4387c34 · 4387c34
1 parent 27e4453
commit 4387c34
Showing 1 changed file with 6 additions and 2 deletions.
diff --git a/developers/docker-ci/Dockerfile b/developers/docker-ci/Dockerfile
@@ -54,8 +54,12 @@ RUN ${SML} < tools/smart-configure.sml
 RUN bin/build ${BUILDOPTS}
 
 # Building HOL manuals when PolyML is used
-RUN if [ "poly" == "${SML}"] ; then \
-    cd Manual && ../bin/Holmake -j2; \
+RUN if [ "poly" = "${SML}" ]; then \
+    if echo ${BUILDOPTS} | grep -q "otknl"; then \
+       echo Skip manual building; \
+    else \
+       cd Manual; ../bin/Holmake -j2; \
+    fi \
 fi
 
 # This can be overrided by "docker run <command>"