From 5b521da5573b3355be41f9025e7c04a2e2270b0c Mon Sep 17 00:00:00 2001
From: Abe Levitan <alevitan@mit.edu>
Date: Wed, 4 Sep 2019 16:37:30 -0400
Subject: [PATCH] Add the publishing script so we can publish the docs to
 github pages on the enterprise server

---
 docs/publish | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100755 docs/publish

diff --git a/docs/publish b/docs/publish
new file mode 100755
index 0000000..377f0db
--- /dev/null
+++ b/docs/publish
@@ -0,0 +1,34 @@
+#!/usr/bin/env bash
+
+# switch branches and make sure we've got the latest version
+git checkout gh-pages
+git pull origin gh-pages
+
+# go to master for the latest docs from master
+git checkout master
+git pull origin master
+
+# build the docs
+make clean
+make html
+cd ..
+
+# switch back to gh-pages
+git checkout gh-pages
+
+# delete everything non-relevant and extract docs
+ls | grep -v docs | xargs rm -r 
+touch .nojekyll
+mv ./docs/build/html/* ./
+rm -rf ./docs
+
+# And commit to publish
+git add -A
+git commit -m "publishing updated docs..."
+git push origin gh-pages
+
+# switch back to master
+git checkout master
+
+# go back to docs dir
+cd docs