Skip building manuals in --otknl mode

binghe · Apr 30, 2024 · 252c722 · 252c722
1 parent 63527fe
commit 252c722
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/developers/docker-ci/Dockerfile b/developers/docker-ci/Dockerfile
@@ -55,7 +55,11 @@ RUN bin/build ${BUILDOPTS}
 
 # Building HOL manuals when PolyML is used
 RUN if [ "poly" = "${SML}" ]; then \
-    cd Manual; ../bin/Holmake -j2; \
+    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>"