Pipe "git merge -q" output to /dev/null since it's not appropriately quiet in the face of file removals

This commit is contained in:
Tianon Gravi 2016-06-03 10:52:03 -07:00
parent 7e46e0cea7
commit 4182896ba7

View file

@ -58,7 +58,7 @@ else
git config user.name 'nobody'
git config user.email 'nobody@nowhere.noplace'
git fetch -q origin "pull/$pull/head:pr-$pull"
git merge -q --no-edit "pr-$pull"
git merge -q --no-edit "pr-$pull" > /dev/null
commit="$(git log -1 --format=format:%h "pr-$pull")"
fi