diff --git a/make-doc.sh b/make-doc.sh new file mode 100644 index 0000000..79c3f53 --- /dev/null +++ b/make-doc.sh @@ -0,0 +1 @@ +scribble --html --dest-name index.html main.rkt diff --git a/push.sh b/push.sh new file mode 100644 index 0000000..3dd633b --- /dev/null +++ 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