site: update deploy script

This commit is contained in:
Simon Michael 2019-02-09 19:48:01 -08:00
parent 1570d5c6df
commit b3dd667feb

View File

@ -19,16 +19,15 @@ git pull && \
# fetch latest wiki content
printf "wiki: " && git -C wiki pull && \
# add latest wiki sidebar links to home page, and push right away so we can keep pulling
make --no-print-directory site/index.md-push && \
# ensure GHC can handle non-ascii
export LANG=en_US.UTF-8 && \
# ensure latest Shake is built
./Shake.hs \
./Shake.hs && \
# update website's generated content (eg manuals) and html
# update website
./Shake site/index.md && \
./Shake website \
# print and log to: