diff options
| author | Théo Zimmermann | 2020-01-07 22:10:39 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-01-07 22:10:39 +0100 |
| commit | d8d5631ed89b645e2bce50203a877ef5b5ab4fab (patch) | |
| tree | 0c88c5826e8bce1ed7345e4d2c80319a70dd96dd /plugins/syntax/float_syntax.ml | |
| parent | cfc41cb79e2364f19d97e7e5c94262132972b0b2 (diff) | |
[merge script] Never bypass outdated branch sanity check.
The message was confusing and the prompt let one reviewer think the
merge script would take care of doing the pull, which it doesn't.
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions