diff options
author | 2018-04-08 20:34:06 +0200 | |
---|---|---|
committer | 2018-04-09 10:17:36 +0200 | |
commit | fe3977512f18c269e82765995ee1e9ba5d6e4b43 (patch) | |
tree | f994ef92c144763beff4a891d6b8d1a081370762 /vernac/indschemes.mli | |
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 'vernac/indschemes.mli')
0 files changed, 0 insertions, 0 deletions