In the end this required a slightly nasty hack using a dummy anchor as an option heading in order to make the "Other recognized __flags__" line indent properly. Fixes bug 11061; Bugfix on 61d740ed.
61d740ed
