commit bc72402949211ed7ddb90805ba132f205c6f9d0e parent dd30807707568996e95cac9782403f65d78f64bb Author: Marcello Stanisci <marcello.stanisci@inria.fr> Date: Wed, 1 Jun 2016 14:56:17 +0200 adding script to update local copy of deployment repo Diffstat:
| A | taler-build/update_deployment.sh | | | 16 | ++++++++++++++++ |
1 file changed, 16 insertions(+), 0 deletions(-)
diff --git a/taler-build/update_deployment.sh b/taler-build/update_deployment.sh @@ -0,0 +1,16 @@ +#!/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