From a5932f7cf7b9283c826bc562f9916e72beeb9b38 Mon Sep 17 00:00:00 2001
From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Wed, 20 Mar 2019 23:36:28 +0000
Subject: [PATCH] Makefile: add git push to publication target

---
 Makefile | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Makefile b/Makefile
index 97f112b..9bc7095 100644
--- 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
-- 
2.30.2