diff options
author | Takeshi KOMIYA <i.tkomiya@gmail.com> | 2020-02-22 14:16:02 +0900 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-22 14:16:02 +0900 |
commit | 723c4491c79111def6932efe6876947361850ff4 (patch) | |
tree | d11a9edcb1111fe1ab75ff3ffceaf41eb576efa8 /sphinx/ext/coverage.py | |
parent | 792b578d4623e302547fb38b6156649b1d9e04d9 (diff) | |
parent | 73fd75f117a950ddc8de20a6a81700162b4057ee (diff) | |
download | sphinx-git-723c4491c79111def6932efe6876947361850ff4.tar.gz |
Merge pull request #7194 from tk0miya/search_show_warning
html search: show warning if [role=main] element not found
Diffstat (limited to 'sphinx/ext/coverage.py')
0 files changed, 0 insertions, 0 deletions