push: support pushing HEAD to real branch name

diff --git a/git-mergetool.sh b/git-mergetool.sh
index a68b40386bde1c47c33a19514ec3a22db7fb0e4b..5587c5ecea0f6a97f2715636890c9e2f89845d52 100755 (executable)
--- a/git-mergetool.sh
+++ b/git-mergetool.sh
@@ -10,6 +10,7 @@
 
 USAGE='[--tool=tool] [file to merge] ...'
 SUBDIRECTORY_OK=Yes
+OPTIONS_SPEC=
 . git-sh-setup
 require_work_tree
 prefix=$(git rev-parse --show-prefix)