From 047772577c1f72411d52a195b6d79c901ab9fa24 Mon Sep 17 00:00:00 2001 From: "Ryan M. Moore" Date: Sun, 31 Oct 2021 00:18:40 -0400 Subject: [PATCH] Update makefile and workflow --- .github/workflows/generate_docs.yml | 4 +++- Makefile | 3 +-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/.github/workflows/generate_docs.yml b/.github/workflows/generate_docs.yml index f725e21..edb8a0a 100644 --- 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 index 7d90c4e..d2719c1 100644 --- 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: