Merge branch 'jk/diff-rendered-docs'
commitf74e7b8c5b1d5d7a70cfd3a747ee7242060092e9
authorJunio C Hamano <gitster@pobox.com>
Fri, 17 Aug 2018 20:09:58 +0000 (17 13:09 -0700)
committerJunio C Hamano <gitster@pobox.com>
Fri, 17 Aug 2018 20:09:58 +0000 (17 13:09 -0700)
tree9c3e63e68b12d5d257b6815114a0571d034c5be7
parentf382c24ef0331d5b56461cb0c0480b58ae75cf7c
parentbeb188e22ad0ca4287984c316c7e0b0f9aa895e6
Merge branch 'jk/diff-rendered-docs'

The end result of documentation update has been made to be
inspected more easily to help developers.

* jk/diff-rendered-docs:
  add a script to diff rendered documentation