diff --git a/marketplace/scribblings/Makefile b/marketplace/scribblings/Makefile index 6748ec1..739491b 100644 --- a/marketplace/scribblings/Makefile +++ b/marketplace/scribblings/Makefile @@ -1,5 +1,15 @@ all: out +pages: + git clone -b gh-pages ../.. pages + +publish: out pages + cp -r out/marketplace/. pages/. + (cd pages; git add -A) + -(cd pages; git commit -m "Update $$(date +%Y%m%d%H%M%S)") + (cd pages; git push) + rm -rf pages + out: raco scribble \ --htmls \ @@ -10,4 +20,4 @@ out: marketplace.scrbl clean: - rm -rf out \ No newline at end of file + rm -rf out