From 2e76ebc72ea00f60adbd17499a3b9bbefd12e10d Mon Sep 17 00:00:00 2001
From: "James D. Mitchell" <jdm3@st-andrews.ac.uk>
Date: Wed, 15 Nov 2023 16:44:32 +0000
Subject: [PATCH] Add script to deploy the doc

---
 .gitignore        |  1 +
 etc/deploy-doc.sh | 28 ++++++++++++++++++++++++++++
 2 files changed, 29 insertions(+)
 create mode 100755 etc/deploy-doc.sh

diff --git a/.gitignore b/.gitignore
index 359907e8..05cdd11f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -36,3 +36,4 @@
 
 TAGS
 build*
+gh-pages
diff --git a/etc/deploy-doc.sh b/etc/deploy-doc.sh
new file mode 100755
index 00000000..09496ef4
--- /dev/null
+++ b/etc/deploy-doc.sh
@@ -0,0 +1,28 @@
+#!/bin/bash
+set -e
+
+if ! [[ -d "gh-pages" ]] ; then
+    echo -e "Error, the \"gh-pages\" directory is not present:"
+    echo -e "git clone --branch=gh-pages git@github.com:libsemigroups/hpcombi.git gh-pages"
+    exit 1 
+fi
+
+printf "\033[0;32mDeploying updates to GitHub...\033[0m\n"
+
+mkdir -p build
+cd build
+if [[ -f Makefile ]] ; then
+  make clean
+fi
+cmake ..
+make doc
+cd ..
+cp -r build/doc/html/* gh-pages
+cd gh-pages
+git add .
+msg="rebuilding site $(date)"
+if [ -n "$*" ]; then
+	msg="$*"
+fi
+git commit -m "$msg"
+# git push origin gh-pages