From 5fc04f8f5c8fee007aaf5679d8de40df331df022 Mon Sep 17 00:00:00 2001 From: Ewen Maclean Date: Wed, 17 Oct 2018 11:11:18 +0100 Subject: [PATCH 1/5] updating doc generation instructions --- INSTALL.md | 8 ++++---- Makefile | 2 ++ 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/INSTALL.md b/INSTALL.md index c4d72942..41e1ef41 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -34,15 +34,15 @@ To update the documentation in the `gh-pages` branch, you can do the following: - stash the changes in the `doc` folder ``` -git add doc/* +git add _pages/doc/* git stash ``` - checkout gh-pages and apply the stash ``` -git checkout gh-pages -git checkout stash -- doc +git checkout gh-pages-src +git checkout stash -- _pages git commit -m "Update documentation" -git push origin gh-pages +git push origin gh-pages-src ``` diff --git a/Makefile b/Makefile index d8118770..3b164ce9 100644 --- a/Makefile +++ b/Makefile @@ -24,6 +24,8 @@ doc: @echo "src-protocol-exts-pp-vg" > dune-ignore @echo "src-protocol-exts-vg" >> dune-ignore dune build @doc + mkdir -p _pages/doc + cp -r _build/default/_doc/_html/* _pages/doc/ rm dune-ignore module_graph.svg: _build/doc/all_modules.docdir/all_modules.dot From abe10ac8325bdab19a1201544521c259ece16f8d Mon Sep 17 00:00:00 2001 From: Ewen Maclean Date: Wed, 17 Oct 2018 12:56:15 +0100 Subject: [PATCH 2/5] updating Makefile not to copy generated odoc css --- Makefile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 3b164ce9..054d0dee 100644 --- a/Makefile +++ b/Makefile @@ -26,6 +26,7 @@ doc: dune build @doc mkdir -p _pages/doc cp -r _build/default/_doc/_html/* _pages/doc/ + rm -rf _pages/doc/odoc.css rm dune-ignore module_graph.svg: _build/doc/all_modules.docdir/all_modules.dot @@ -60,7 +61,7 @@ _opam: opam install -y ocaml-base-compiler.4.05.0 clean: - duneer clean + dune clean .PHONY: build build_vgs run run_server clean doc From 255960803bd690f88b7e28f5c2e4a6c2c1cd80a7 Mon Sep 17 00:00:00 2001 From: Ewen Maclean Date: Wed, 17 Oct 2018 13:17:53 +0100 Subject: [PATCH 3/5] updating makefile to do nav replacement using sed in makefile --- Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/Makefile b/Makefile index 054d0dee..ff6984b2 100644 --- a/Makefile +++ b/Makefile @@ -27,6 +27,7 @@ doc: mkdir -p _pages/doc cp -r _build/default/_doc/_html/* _pages/doc/ rm -rf _pages/doc/odoc.css + sed -i '' -e 's//