tree a974ee6fc7fc745081d5a2e90e570fc0247b295f
parent 60aced3dfa68df60952fed28c4ae63a5bbda0275
author Denton Liu <liu.denton@gmail.com> 1556518877 -0400
committer Junio C Hamano <gitster@pobox.com> 1557756719 +0900

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>