Merge branch 'js/push-to-deploy'

"git push" into a repository with a working tree normally refuses
to modify the branch that is checked out.  The command learned to
optionally do an equivalent of "git reset --hard" only when there
is no change to the working tree and the index instead, which would
be useful to "deploy" by pushing into a repository.

* js/push-to-deploy:
t5516: more tests for receive.denyCurrentBranch=updateInstead
receive-pack: add another option for receive.denyCurrentBranch

diff --cc Documentation/config.txt
Simple merge

diff --cc builtin/receive-pack.c
Simple merge