mirror of
https://github.com/dlang/dmd.git
synced 2025-04-26 21:21:48 +03:00
Use GitHub's merge head for checking out PRs
This commit is contained in:
parent
82c2ebef38
commit
366fee847b
2 changed files with 4 additions and 7 deletions
|
@ -18,10 +18,10 @@ jobs:
|
|||
name: Install GDB
|
||||
- run:
|
||||
command: ./.circleci/run.sh setup-repos
|
||||
name: Clone DMD & DRuntime
|
||||
name: Clone DRuntime & Phobos
|
||||
- run:
|
||||
command: ./.circleci/run.sh coverage
|
||||
name: Run Phobos testsuite with -cov
|
||||
name: Run testsuite with -cov
|
||||
- run:
|
||||
command: ./.circleci/run.sh check-clean-git
|
||||
name: Check for temporary files generated by the test suite
|
||||
|
|
|
@ -74,12 +74,9 @@ setup_repos() {
|
|||
# merge testee PR with base branch (master) before testing
|
||||
if [ -n "${CIRCLE_PR_NUMBER:-}" ]; then
|
||||
local head=$(git rev-parse HEAD)
|
||||
git fetch https://github.com/dlang/$CIRCLE_PROJECT_REPONAME.git $base_branch
|
||||
git remote add upstream "https://github.com/dlang/$CIRCLE_PROJECT_REPONAME.git"
|
||||
git fetch -q upstream "+refs/pull/${CIRCLE_PR_NUMBER}/merge:"
|
||||
git checkout -f FETCH_HEAD
|
||||
local base=$(git rev-parse HEAD)
|
||||
git config user.name 'CI'
|
||||
git config user.email '<>'
|
||||
git merge -m "Merge $head into $base" $head
|
||||
fi
|
||||
|
||||
for proj in druntime phobos; do
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue