From d4e0a891c03dbc8a96cee6a25be4950a28f072be Mon Sep 17 00:00:00 2001 From: Laurent Rineau Date: Fri, 30 Nov 2012 11:17:49 +0100 Subject: [PATCH] git pull is not robust. Now I use `git rev-parse --abbrev-rev HEAD` to get the branch name, and then `git reset --hard` to force the update to the last revision of the branch. --- .../cgal.geometryfactory.com/bin/create_release | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Maintenance/infrastructure/cgal.geometryfactory.com/bin/create_release b/Maintenance/infrastructure/cgal.geometryfactory.com/bin/create_release index 5a5500543f9..bf3f69c882e 100755 --- a/Maintenance/infrastructure/cgal.geometryfactory.com/bin/create_release +++ b/Maintenance/infrastructure/cgal.geometryfactory.com/bin/create_release @@ -5,7 +5,10 @@ export LC_ALL if [ -d "$1/.git" ]; then pushd $1 - git pull + branch=`git rev-parse --abbrev-ref HEAD` + echo "Git repository, in branch '$branch'" + git fetch + git reset --hard origin/$branch popd else svn up "$1"