From 7097c88d3b877690e95dc927b3575940a4f954ff Mon Sep 17 00:00:00 2001 From: Robur Date: Wed, 15 Nov 2023 10:04:02 +0000 Subject: [PATCH] add update script --- update.sh | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100755 update.sh diff --git a/update.sh b/update.sh new file mode 100755 index 0000000..90ab3ab --- /dev/null +++ b/update.sh @@ -0,0 +1,6 @@ +#!/bin/sh + +opam exec -- dune exec src/blogger.exe -- push \ + -r git@git.robur.coop:robur/blog.robur.coop.git#gh-pages \ + --name "The Robur team" \ + --email team@robur.coop