diff --git a/.github/scripts/main/main.sh b/.github/scripts/main/main.sh index 65030b288a9..a057081bf7a 100644 --- a/.github/scripts/main/main.sh +++ b/.github/scripts/main/main.sh @@ -90,6 +90,8 @@ if [ "$OPAM_DOC" = "1" ]; then doc/html/opam-solver/index.html doc/html/opam-state/index.html + nonexistent.ml + doc/pages/Install.html doc/pages/Install.md doc/man-html/opam-init.html"