From 656565c1957da549ddec6498e640fe9c8e58eb4f Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 22 Aug 2016 10:15:37 +0200 Subject: [PATCH] add gh-pages doc generation to makefile --- Makefile | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Makefile b/Makefile index ed28398b..00dd73da 100644 --- a/Makefile +++ b/Makefile @@ -55,6 +55,13 @@ examples: all push_doc: doc rsync -tavu containers.docdir/* cedeela.fr:~/simon/root/software/containers/ +push_doc_gh: doc + git checkout gh-pages && \ + rm -rf dev/ && \ + mkdir -p dev && \ + cp -r containers.docdir/* dev/ && \ + git add --all dev + DONTTEST=myocamlbuild.ml setup.ml $(wildcard src/**/*.cppo.*) QTESTABLE=$(filter-out $(DONTTEST), \ $(wildcard src/core/*.ml) \