From 17834d531ccab4bdd307253fc6d501d6e2216bde Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Wed, 24 Jul 2013 06:33:01 -0700
Subject: [PATCH] Add update_doxygen.sh script and use it in .travis.yml

---
 .travis.yml              |  5 ++++-
 script/update_doxygen.sh | 33 +++++++++++++++++++++++++++++++++
 2 files changed, 37 insertions(+), 1 deletion(-)
 create mode 100755 script/update_doxygen.sh

diff --git a/.travis.yml b/.travis.yml
index 9a15e9a908..3c97afda03 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -36,7 +36,10 @@ before_script:
 script:
   - make
   - ctest -T test -VV
-  - cd ..; if [[ $BUILD_DOXYGEN == TRUE ]]; then sudo apt-get -qq install doxygen graphviz; doxygen src/Doxyfile; COMMIT_LOG=`git log --oneline -n 1`; git config user.email "soonhok@cs.cmu.edu"; git config user.name "Soonho Kong"; git checkout -B gh-pages gh-pages; git add -A doc;  git commit -m "Update doxygen - $COMMIT_LOG"; git push origin gh-pages; git checkout master; fi
+
+after_success:
+  - cd ..
+  - if [[ $BUILD_DOXYGEN == TRUE ]]; then ./script/update_doxygen.sh; fi
 
 install:
   - sudo add-apt-repository --yes ppa:ubuntu-toolchain-r/test
diff --git a/script/update_doxygen.sh b/script/update_doxygen.sh
new file mode 100755
index 0000000000..c1aeebc8d5
--- /dev/null
+++ b/script/update_doxygen.sh
@@ -0,0 +1,33 @@
+#!/usr/bin/env bash
+#
+# update_doxygen.sh:
+#       1) Install and run doxygen
+#       2) Push the result to gh-pages branch
+#
+# author: Soonho Kong
+#
+if [ "$TRAVIS_PULL_REQUEST" == "false" ]; then
+    echo -e "Starting to generate doxygen pages"
+    sudo apt-get -qq install doxygen graphviz;
+    doxygen src/Doxyfile;
+    COMMIT_LOG=`git log --oneline -n 1`;
+    mv doc $HOME
+    echo -e "Done.\n"
+
+    echo -e "Starting to update gh-pages\n"
+    #go to home and setup git
+    cd $HOME
+    git config --global user.email "travis@travis-ci.org"
+    git config --global user.name "Travis"
+
+    #using token clone gh-pages branch
+    git clone --quiet --branch=gh-pages https://${GH_TOKEN}@github.com/leodemoura/lean.git  gh-pages > /dev/null
+    #go into diractory and copy data we're interested in to that directory
+    cd gh-pages
+    mv -Rf $HOME/doc .
+    #add, commit and push files
+    git add -A doc
+    git commit -m "Push doxygen for the commit -- $COMMIT_LOG -- to gh-pages"
+    git push -fq origin gh-pages > /dev/null
+    echo -e "Done.\n"
+fi