diff options
author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-08 20:34:06 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-09 10:17:36 +0200 |
commit | fe3977512f18c269e82765995ee1e9ba5d6e4b43 (patch) | |
tree | f994ef92c144763beff4a891d6b8d1a081370762 /clib | |
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 'clib')
0 files changed, 0 insertions, 0 deletions