We had a PR to fix those just recently - the {} is needed to produce space. \opt doesn't use anything fancy like \xspace.

We should use \opt{} everywhere to avoid the possibility of problems / missing whitespace.

Should we instead add \xspace to \opt so that it acts like \opt{}?

I'm really worried about xspace because I don't really understand how it interacts with other punctuators. I'd be perfectly happy to use \opt{} when necessary.

On 23 Jun 2016 12:03 a.m., "burblebee" notifications@github.com wrote:

Should we instead add \xspace to \opt so that it acts like \opt{}?

I'd like to move away from xspace. It's too unpredictable.

—
You are receiving this because you commented.

Reply to this email directly, view it on GitHub, or mute the thread.

OK. Shall I turn all \opts into \opt{}s then? Or leave as is and close this issue as "NAD"?

Well, is the spacing actually wrong? I'd say we should have the {} if and only if it's needed.

Great - let's close this as a non-issue then.