From bc72402949211ed7ddb90805ba132f205c6f9d0e Mon Sep 17 00:00:00 2001
From: Marcello Stanisci <marcello.stanisci@inria.fr>
Date: Wed, 1 Jun 2016 14:56:17 +0200
Subject: adding script to update local copy of deployment repo

---
 taler-build/update_deployment.sh | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100755 taler-build/update_deployment.sh

diff --git a/taler-build/update_deployment.sh b/taler-build/update_deployment.sh
new file mode 100755
index 0000000..c3aa3c5
--- /dev/null
+++ 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
-- 
cgit v1.2.3