From: Gereon Kremer <nafur42@gmail.com>
Date: Mon, 20 Sep 2021 16:12:57 +0000 (+0200)
Subject: Add anchors to cmdline options (#7210)
X-Git-Tag: cvc5-1.0.0~1196
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=656b13b04627a7c226fb6367ca4323c4971d5f48;p=cvc5.git

Add anchors to cmdline options (#7210)

This PR adds anchors to the auto-generates command line option documentation. This allows to link to specific options from other parts of the documentation.
---

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index c12a54ebb..a8f631de6 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -784,6 +784,7 @@ def _sphinx_help_add(module, option, common, others):
             modes[data[0]['name']] = data[0].get('help', '')
 
     data = {
+        'long_name': option.long_name,
         'name': names,
         'help': option.help,
         'expert': option.category == 'expert',
@@ -805,6 +806,8 @@ def _sphinx_help_render_option(res, opt):
     indent = ' ' * 4
     desc = '``{}``'
     val = indent + '{}'
+    res.append('.. _lbl-option-{}:'.format(opt['long_name']))
+    res.append('')
     if opt['expert']:
         res.append('.. admonition:: This option is intended for Experts only!')
         res.append(indent)