#!/bin/bash

# This update script is needed since shell scripts called
# by buildbot do NOT use the fresh deployment repo which is
# internal to buildbot, so we need to update the $HOME/deployment
# local check before starting the whole compilation

set -eu

cd $HOME/deployment
git clean -fdx

# like "git pull", but robust against force pushes
# and local changes
git fetch
git reset --hard FETCH_HEAD