diff options
| author | Théo Zimmermann | 2018-04-08 20:34:06 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-04-09 10:17:36 +0200 |
| commit | fe3977512f18c269e82765995ee1e9ba5d6e4b43 (patch) | |
| tree | f994ef92c144763beff4a891d6b8d1a081370762 /dev/ci/ci-basic-overlay.sh | |
| parent | ff223fac386ab4d0e622d1dc03d47cff34db3311 (diff) | |
Add sanity check in merge script: local branch is up-to-date.
In case the local branch is ahead of upstream, we only print
a warning because it could be that we are merging several
PRs in a row.
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
0 files changed, 0 insertions, 0 deletions