Re: makeinfo and CSS

[Karl Berry]

    pre.smallexample { font-size: inherit ! important }

You are a wizard :).

We could always add the explicit option (--css-omit-defaults) to skip
inserting the defaults, if it turns out to be necessary.

    Yes, but it is not only easy to find the *start* of an @import rule,
    but also its end, because it must be a ";" (you must skip one string
    though).  Many @import rules may be present, but nothing inbetween,
    not even other @... rules.

Thanks for the info.  Do you feel like writing the code, by any chance :)?

    It would be nice if eventually one CSS command line option for
    makeinfo turns out to be sufficient.

Yes, I agree that's cleaner.

Thanks,
karl