doc: Fix Typesetting of "--"
In the HTML output, the Scribble source --
becomes an en-dash, which is
confusing. Does one use the same idiom in Scribble that one uses in TeX to
prevent this, i.e., -{}-
?
In the HTML output, the Scribble source --
becomes an en-dash, which is
confusing. Does one use the same idiom in Scribble that one uses in TeX to
prevent this, i.e., -{}-
?