#!/bin/sh
export PATH=/usr/local/bin/:$PATH

git remote update 1>/dev/null

LOCAL=$(git rev-parse @{0})
REMOTE=$(git rev-parse @{u})

if [ $LOCAL != $REMOTE ]; then
    git pull
    PATH="/usr/local/bin:$PATH" make COQWEB=/srv/coq-www/www all
fi

#!/bin/sh
export PATH=/usr/local/bin/:$PATH

git remote update 1>/dev/null

LOCAL=$(git rev-parse @{0})
REMOTE=$(git rev-parse @{u})

if [ $LOCAL != $REMOTE ]; then
    git pull
    PATH="/usr/local/bin:$PATH" make COQWEB=/var/deploy/coq-www all
fi

Update locations for new infrastructure
Update locations for new infrastructure

I doubt this script should be part of the repo. As of today, it is
served, and in case of self-upgrade, things will derail quickly...
