docs: Replace – with -- in HTML documentation

When generating the HTML documentation, the sequence `--` in option
names is replaced by the HTML entity `–`. This results in
erroneous documentation: if someone were to copy and paste an option
from the HTML man page, it would result in an error.

Author: larsks