From 7f428b6f663146114fe77491069412d190dcb411 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 13 Jul 2022 10:27:52 +0200 Subject: [PATCH] prefix everything with opam exec --- .github/workflows/docs.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 40d8979a0..c2323f75e 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -26,9 +26,9 @@ jobs: - run: eval $(opam env) - name: Install and Build 🔧 # This example project is built using npm and outputs the result to the 'build' folder. Replace with the commands required to build your project, or remove this step entirely if your site is pre-built. run: | - ./configure - make - make doc + opam exec -- ./configure + opam exec -- make + opam exec -- make doc - name: Deploy 🚀 uses: JamesIves/github-pages-deploy-action@v4