Re: HTML file name change in 4.7?

[Patrice Dumas]

>     (Btw, does the scheme handle Unicode code points > 0xffff?)
> 
> Apparently not :(.  Patrice?

Indeed it does not. I thought there was nothing above 0xffff... 
I had a look at the standard. The code points above 0xffff aren't that 
important, but they must be considered (would be nice a texinfo manual in
gothic :). If I'm not wrong there are no code point above 0xffffff... I
hope I'm not wrong now...

Now to include that in the proposal there are 2 possibilities:
1) use now _xxxxxx instead of _xxxx. It is not backward compatible and adds
   unusefull xx which will be 00 in 99,999999% of the case.
2) Still use _xxxx for codepoints below 0xffff, but use __xxxxxx for 
   codepoints above 0xffff. Backward compatible, but add a _ which is rather 
   ugly if the text is full of codepoints above 0xffff. Another issue is that 
   it may add more complexity in the code.

I personnaly prefer the solution 2), but not firmly. Karl and others ?

Pat