users-guide: Fix various bits of markup
authorBen Gamari <ben@smart-cactus.org>
Thu, 14 Dec 2017 21:52:59 +0000 (16:52 -0500)
committerBen Gamari <ben@smart-cactus.org>
Thu, 14 Dec 2017 22:03:46 +0000 (17:03 -0500)
commit4a331e659f636e28330142b6df90cb0772a19463
tree432589485f8d71da757b2091040f89d5edc1aae6
parentd4c8d895a477e66cc5d892de7d5f06a4068f9244
users-guide: Fix various bits of markup

(cherry picked from commit 15b2b959abbc724187b0e58979968d24ab323681)
docs/users_guide/8.4.1-notes.rst
docs/users_guide/separate_compilation.rst