1284

1 files changed, 11 insertions, 0 deletions

diff --git a/update_github_page b/update_github_page
new file mode 100755
index 00000000..6925354b
--- /dev/null
+++ b/update_github_page
@@ -0,0 +1,11 @@
+#!/bin/bash
+#
+# Github populates http://akkartik.github.io/mu with branch gh-pages
+# (More info: https://pages.github.com)
+# We keep gh-pages sync'd with master.
+
+git checkout gh-pages
+git pull . master
+git push
+git checkout master
+git push