merge -p "$src1" "$orig" "$src2" > "$4"
ret=$?
rm -f -- "$orig" "$src1" "$src2"
+
if [ "$6" != "$7" ]; then
echo "ERROR: Permissions $5->$6->$7 don't match."
ret=1
fi
+ case "$6" in *7??) mode=+x;; *) mode=-x;; esac
+ chmod "$mode" "$4"
+
if [ $ret -ne 0 ]; then
# Reset the index to the first branch, making
# git-diff-file useful