Update makefile and workflow

mooreryan · Oct 31, 2021 · 0477725 · 0477725
1 parent e6b9b21
commit 0477725
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/.github/workflows/generate_docs.yml b/.github/workflows/generate_docs.yml
@@ -25,7 +25,9 @@ jobs:
 
       - run: opam install . --deps-only --with-doc --with-test
 
-      - run: make docs_site
+      - run: opam exec -- make build
+      - run: opam exec -- make docs_site
+
       - run: git checkout gh-pages
       - run: if [ -d docs ]; then rm -r docs; fi
       - run: mv _docs docs

diff --git a/Makefile b/Makefile
@@ -16,8 +16,7 @@ docs_site:
 	if [ -d $(DOCS_D) ]; then rm -rf $(DOCS_D); fi
 	dune build @doc && \
 	  mv _build/default/_doc/_html docs && \
-	  chmod 755 $(DOCS_D) && \
-	  $(BROWSER) ./$(DOCS_D)/index.html
+	  chmod 755 $(DOCS_D)
 
 .PHONY: test
 test: