Fix API site build (#8551)
authorPaul Ouellette <oue.paul18@gmail.com>
Tue, 21 May 2019 17:37:10 +0000 (13:37 -0400)
committerSmallJoker <SmallJoker@users.noreply.github.com>
Tue, 21 May 2019 17:37:10 +0000 (19:37 +0200)
commit920bd3b16fd0aaafd9eeb6d8e40310664d1a06dc
treed52e99bcd2435b6a4d0fe8b2f54f10aff64eb754
parentcfef466d4ef2eee5586bbd8afacc64e4a1939d88
Fix API site build (#8551)
doc/mkdocs/build.sh
doc/mkdocs/code_tag.patch [deleted file]
doc/mkdocs/lua_highlight.patch