Commit 8e4afd31 authored by Ondřej Surý's avatar Ondřej Surý
Browse files

Merge branch '1898-doc/misc/options-should-be-independent-on-configure' into 'main'

Remove // not configured when generating doc/misc/options

Closes #1898

See merge request !3731
parents c3510ca6 b82ff5b7
Pipeline #44922 passed with stages
in 3 minutes and 9 seconds