Re: CSS file for texinfo HTML output

[Karl Berry]

    For reference, here's the CSS standard on the definition of a pixel:

I see, so they've changed "px" to be a nominal device-independent pixel
instead of a real pixel, as it always was before.  I didn't know that.
I wonder how many, if any, browsers today actually implement it, though.

I still don't see why pt is a problem, and presumably pt works (is
device-independent) in more browsers today, but maybe they redefined
that too.  Whatever.

Thanks for the info,
Karl