makeinfo split html on mac os x

[Trevis Rothwell]

Running makeinfo on Mac OS X, to get a split-by-node set of HTML files, e.g.:

  makeinfo --html --output=html_node gnu-c-manual.texi

Some of the HTML toward the end of the inline CSS block at the top gets
mysteriously jumbled:

  <style type="text/css"><!--
    pre.display { font-family:inherit }
    pre.format  { font-family:inherit }
    pre.smalldisplay { font-family:inherit; font-size:smaller }
    pre.smallformat  { font-family:inherit; font-size:smaller }
    pre.smallexample { font-size:smaller }
    pre.smalllisp    { font-size:smaller }
    span.sc { font-varia<div class="contents">
  <h2>Table of Contents</h2>

(Look at the last two lines specifically.)

The same results happened using makeinfo 4.7 and makeinfo 4.9.  The --no-split
option generates correct HTML output.

Using makeinfo 4.8 on GNU/Linux (specifically, on fencepost) resulted
in correct HTML output, given the same Texinfo source.