diff options
Diffstat (limited to 'utils/makefile.sphinx')
| -rw-r--r-- | utils/makefile.sphinx | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/utils/makefile.sphinx b/utils/makefile.sphinx index 01181ff27..5cbc5ebdd 100644 --- a/utils/makefile.sphinx +++ b/utils/makefile.sphinx @@ -194,20 +194,20 @@ $(BOOKS_CLEAN): # github pages PHONY += $(GH_PAGES) -$(GH_PAGES): +$(GH_PAGES):: $(MAKE) docs [ -d "gh-pages/.git" ] || git clone $(GIT_URL) gh-pages - -cd $(GH_PAGES); git checkout --orphan gh-pages || exit 0 - rm -rf $(GH_PAGES)/* $(GH_PAGES)/.gitignore - touch $(GH_PAGES)/.nojekyll ;\ + -cd $(GH_PAGES); git checkout gh-pages >/dev/null + -cd $(GH_PAGES); ls -A | grep -v '.git$$' | xargs rm -rf cp -r $(DOCS_DIST)/* $(GH_PAGES)/ + touch $(GH_PAGES)/.nojekyll echo "<html><head><META http-equiv='refresh' content='0;URL=index.html'></head></html>" > $(GH_PAGES)/404.html - -cd $(GH_PAGES); git push origin :gh-pages cd $(GH_PAGES);\ git add --all . ;\ git commit -m "gh-pages: updated" ;\ git push origin gh-pages + PHONY += docs-clean docs-clean: $(BOOKS_CLEAN) $(call cmd,sphinx_clean) |