We were trying to have jenkins checkout the proper PR branch but the ci script already does this.
The CI script just needs a copy of itself from master, and it will do the right thing.
1 new commit added
rebased onto 5362ad6897cf8765c21040f88245d4f065f20d5c
Commit 44116ae9 fixes this pull-request
Pull-Request has been merged by pingou
We were trying to have jenkins checkout the proper PR branch but the ci script already does this.
The CI script just needs a copy of itself from master, and it will do the right thing.