Merge branch 'ao/config-api-doc'
authorJunio C Hamano <gitster@pobox.com>
Wed, 23 May 2018 05:38:10 +0000 (14:38 +0900)
committerJunio C Hamano <gitster@pobox.com>
Wed, 23 May 2018 05:38:10 +0000 (14:38 +0900)
Doc update.

* ao/config-api-doc:
doc: fix config API documentation about config_with_options

Trivial merge