Merge branch 'master' into gh-pages

2012-10-24 20:35:05 -04:00 · 2012-10-24 20:35:05 -04:00 · c94aad777c
commit c94aad777c
parent ee59ffb8e9 f40c6b407d
1 changed files with 1 additions and 0 deletions
--- a/push.sh
+++ b/push.sh
@ -1,3 +1,4 @@
+# Simply make gh-pages branch a mirror of master branch.
 git checkout master && \
 git push origin master && \
 git checkout gh-pages && \