commit e4641a4076f16d0d27b513e7f9e9351c19f35c24 parent 6d06141751f158b3d1a2699f6e4bc5ddb635e19c Author: Greg Hendershott <greghendershott@gmail.com> Date: Wed, 24 Oct 2012 20:32:27 -0400 Add some scripts Diffstat:
| A | make-doc.sh | | | 1 | + |
| A | push.sh | | | 6 | ++++++ |
2 files changed, 7 insertions(+), 0 deletions(-)
diff --git a/make-doc.sh b/make-doc.sh @@ -0,0 +1 @@ +scribble --html --dest-name index.html main.rkt diff --git a/push.sh b/push.sh @@ -0,0 +1,6 @@ +git checkout master && \ +git push origin master && \ +git checkout gh-pages && \ +git merge master && \ +git push origin gh-pages && \ +git checkout master