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..ff6984b2 100644 --- a/Makefile +++ b/Makefile @@ -24,6 +24,10 @@ 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 -rf _pages/doc/odoc.css + sed -i '' -e 's//