9 @echo 'git clone --branch=gh-pages https://$$(GH_TOKEN)@github.com/cc65/cc65.git $(GH_PAGES)'
10 @git clone --branch=gh-pages https://$(GH_TOKEN)@github.com/cc65/cc65.git $(GH_PAGES)
11 cd $(GH_PAGES) && git config user.name "Oliver Schmidt"
12 cd $(GH_PAGES) && git config user.email "ol.sc@web.de"
13 cd $(GH_PAGES) && git config push.default simple
14 cd $(GH_PAGES) && $(RM) -r doc
15 cd $(GH_PAGES) && mkdir doc
16 cp html/*.* $(GH_PAGES)/doc
17 cd $(GH_PAGES) && git add -A doc
18 cd $(GH_PAGES) && git commit -m "Updated from commit $(TRAVIS_COMMIT)."
19 -cd $(GH_PAGES) && git push