projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e398f79) | patch
Improve rendering of expert options. (#7589)
authorGereon Kremer <nafur42@gmail.com>
Mon, 8 Nov 2021 23:37:10 +0000 (15:37 -0800)
committerGitHub <noreply@github.com>
Mon, 8 Nov 2021 23:37:10 +0000 (23:37 +0000)
commit5094ea8462bdcc61bf9173545cea7aa290fc5ea5
tree310625a133f55ca54b4964fba12ba5ec372a0a52tree
parente398f79c61304378cc736828632a462c74ce39d2commit | diff
Improve rendering of expert options. (#7589)

The way expert-only options have been rendered in the documentation emphasized those options, which is exactly what should not be done. This PR changes the rendering to make those options slightly opaque instead.
docs/_static/custom.css diff | blob | history
src/options/mkoptions.py diff | blob | history