diff options
| author | Guillaume Melquiond | 2019-03-26 11:25:13 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2019-03-26 11:25:13 +0100 |
| commit | 9c821d8dde1d6173a1f2a92f8c98c1c61d81c3c6 (patch) | |
| tree | 490e141916632a242b65e609dd7a4eb8aca455ef /kernel/nativelambda.mli | |
| parent | a59d80d3d482813b3c3c1ebce18ae39c3d09e5be (diff) | |
Improve the backport script.
It now uses the origin/master branch rather than the master branch, thus
avoiding the need for local merges.
More importantly, it no longer creates a subshell in case of conflicts,
but instead gives control back to the user. Once conflicts are solved, it
suffices to relaunch the script (instead of exiting the subshell). The
reason is that, otherwise, there was no sane way of giving up a backport,
due to the infinite subshell loop.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions
