Keep git push happy.

diff --git a/doc/Makefile b/doc/Makefile
index dc6c451cf6624311335fadf505cd41367e7d9536..1e2bf435fc15c6f7276a78bd9bb6f40cacae2f0c 100644 (file)
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -35,6 +35,7 @@ ifdef GH_TOKEN
        git clone --branch=gh-pages https://$(GH_TOKEN)@github.com/oliverschmidt/cc65.git $(GH_PAGES)
        git --work-tree=$(GH_PAGES) --git-dir=$(GH_PAGES)/.git config user.name "Oliver Schmidt"
        git --work-tree=$(GH_PAGES) --git-dir=$(GH_PAGES)/.git config user.email "ol.sc@web.de"
+       git --work-tree=$(GH_PAGES) --git-dir=$(GH_PAGES)/.git config push.default simple
        $(RM) -r $(GH_PAGES)/doc
        mkdir $(GH_PAGES)/doc
        cp ../html/* $(GH_PAGES)/doc