UI: merge selection requires merge command instead of preference #185
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This change depends on PR #184 and is part of a solution to the issue #183
("UI: cannot forcibly merge path from UI if merge option not already set").
Together with assoc patterns (PR #178) and with its dependency (PR #184) that
makes the mergeability be verified by the UI it fixes the issue (implementing
solution 2. to the sub-issue 1.).
It prevents paths not having merge commands from being selected for merging
(either by default or in the UI) but do not require the merge preference to be
set anymore.
It can be merged wihtout/before PR #178 and its dependencies to simply make
the verification of mergeability stricter (as without del/assoc patterns when
a command is provided, the merge preference is also set).