Allow set_option documentation #712
Description
We should have a role that allows parsing of set_option commands in the manual.
{{ message }}
Allow
set_option documentation #712We should have a role that allows parsing of set_option commands in the manual.