projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 84a9543) | patch
Add anchors to cmdline options (#7210)
authorGereon Kremer <nafur42@gmail.com>
Mon, 20 Sep 2021 16:12:57 +0000 (18:12 +0200)
committerGitHub <noreply@github.com>
Mon, 20 Sep 2021 16:12:57 +0000 (09:12 -0700)
commit656b13b04627a7c226fb6367ca4323c4971d5f48
treefaf964555bc9b32b3412172946c9be2dd15855actree
parent84a95435ef3d92ea6ee969a574b9fa98d569f93fcommit | diff
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.
src/options/mkoptions.py diff | blob | history