On Fri, Feb 17, 2017 at 4:59 PM, Eric Engestrom wrote:
> Hey all,
>
> I (finally) set up the git hook, which means that the website [1] is now
> automagically updated whenever a change in docs/* on master is pushed.
>
> There might be bugs, and I'll be doing some other git hook related
> changes l
Hey all,
I (finally) set up the git hook, which means that the website [1] is now
automagically updated whenever a change in docs/* on master is pushed.
There might be bugs, and I'll be doing some other git hook related
changes later on; if you see anything weird when pushing or if the
website's
