Remove // not configured when generating doc/misc/options
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.
Closes #1898 (closed)