diff --git a/tools/merge-development-with-master.sh b/tools/merge-development-with-master.sh index 84015f5133..8d2c7f0d8d 100755 --- a/tools/merge-development-with-master.sh +++ b/tools/merge-development-with-master.sh @@ -5,6 +5,7 @@ if [ "$TRAVIS_BRANCH" != "development" ]; then exit 0; fi +git update-ref HEAD master git checkout master git merge "${TRAVIS_COMMIT}" git push "https://${GH_TOKEN}@github.com/babel/babel"