Makefile: add git push to publication target

diff --git a/Makefile b/Makefile
index 97f112b4b8c828e7c62b8ecc535f34fca77096be..9bc7095aed268def55cc7437e15b615e3c15c27c 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -117,6 +117,7 @@ html: $(PDFS) $(PREVIEWS) README map.plag
        cp $^ $@.tmp/ && $i
 
 to-www: html
+       git-push
        rsync -aH --delete html/. $(www)/.
 
 # create opt.plag.reuse to shortcut this