diff options
| author |  Denton Liu <liu.denton@gmail.com> | 2019-04-29 02:21:17 -0400 |
|---|---|---|
| committer |  Junio C Hamano <gitster@pobox.com> | 2019-05-13 23:11:59 +0900 |
| commit | 7f978d7d10a87c4a56ea3101b936cddb25bbe2c6 (patch) | |
| tree | a974ee6fc7fc745081d5a2e90e570fc0247b295f /gpg-interface.h | |
| parent | mergetool: fallback to tool when guitool unavailable (diff) | |
| download | tgif-7f978d7d10a87c4a56ea3101b936cddb25bbe2c6.tar.xz | |
difftool: make --gui, --tool and --extcmd mutually exclusive
In git-difftool, these options specify which tool to ultimately run. As
a result, they are logically conflicting. Explicitly disallow these
options from being used together.
Signed-off-by: Denton Liu <liu.denton@gmail.com>
Signed-off-by: Junio C Hamano <gitster@pobox.com>
Diffstat (limited to 'gpg-interface.h')
0 files changed, 0 insertions, 0 deletions