From d8e6b83987b7a9457b3276edc5b2393099fbdad2 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 13 Sep 2023 23:31:30 -0400 Subject: [PATCH] CI --- .github/workflows/gh-pages.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/gh-pages.yml b/.github/workflows/gh-pages.yml index 68ed803..87c642e 100644 --- a/.github/workflows/gh-pages.yml +++ b/.github/workflows/gh-pages.yml @@ -33,7 +33,7 @@ jobs: run: opam install -d . --deps-only - name: Build - run: opam exec -- dune build @doc + run: opam exec -- dune build @doc --ignore-promoted-rules - name: Deploy uses: peaceiris/actions-gh-pages@v3