Merge branch 'ew/update-server-info'
commit813a3a2ab7b29ad003fc6b8e9b3c4b9421dd36d5
authorJunio C Hamano <gitster@pobox.com>
Thu, 13 Jun 2019 20:19:42 +0000 (13 13:19 -0700)
committerJunio C Hamano <gitster@pobox.com>
Thu, 13 Jun 2019 20:19:42 +0000 (13 13:19 -0700)
treea0d389c9cfd0b3a0956901d752e314e31d752e4a
parent8d32d2552ee476917d216ae584d3d9b9002844d3
parentf4f476b6a19217b6ed3d5022422b3fa0f55a5ee9
Merge branch 'ew/update-server-info'

"git update-server-info" learned not to rewrite the file with the
same contents.

* ew/update-server-info:
  update-server-info: avoid needless overwrites