The doc/misc/options is used to generate a file describing all
configuration options. Currently, the file contents could differ
based on ./configure option which is kind of suboptimal.
We already removed the "// not configured" from the options.active, and
this time we remove generation of the string altogether.
b82ff5b738