2018-05-02 10:03:40 +00:00
|
|
|
#!/bin/sh
|
|
|
|
|
|
|
|
org="$1"
|
|
|
|
repo="$2"
|
|
|
|
|
2018-05-02 15:49:08 +00:00
|
|
|
rm -r "$repo" || true
|
|
|
|
|
2018-12-20 22:13:40 +00:00
|
|
|
clone() {
|
|
|
|
branch=$1
|
|
|
|
if [ -n "$branch" ]
|
|
|
|
then
|
|
|
|
echo "Trying to use the branch $branch"
|
|
|
|
git clone https://github.com/$org/$repo.git $repo --branch "$branch" && exit 0
|
|
|
|
fi
|
|
|
|
}
|
2018-05-02 14:53:38 +00:00
|
|
|
|
2018-12-20 22:13:40 +00:00
|
|
|
# Try the PR author's branch in case it exists on the deps as well.
|
|
|
|
clone $TRAVIS_PULL_REQUEST_BRANCH
|
|
|
|
# Try the target branch of the push or PR.
|
|
|
|
clone $TRAVIS_BRANCH
|
|
|
|
# Try the current branch from Jenkins.
|
|
|
|
clone `"echo $GIT_BRANCH" | sed -e 's/^origin\///'`
|
|
|
|
# Use develop as the last resort.
|
|
|
|
clone develop
|