raw text and @macro

[Karl Berry]

Patrice,

A friend wanted to use the times symbol ($\times$ in TeX, × in
HTML aka ×) in a Texinfo document.  (Aside: we should perhaps add
this particular symbol to the language, or a way to generate any Unicode
char [not possible for TeX, but anyway], but that's a different discussion.)

Given the state of things, the only way I could find to do this within
Texinfo is using @macro, unfortunately:

@tex
@macro xtimes
@math{\times}
@end macro
@end tex

That works ok for TeX.  But for HTML:

@html
@set vtimes ×
@macro xtimes
×
@end macro
@end html

It seems that the raw-ness is lost while handling @set and @macro.
The HTML output from both @value{vtimes} and @xtimes{} looks like:
  ×

Am I missing something?  Is there a workable approach?

Thanks,
Karl