<div id=header>
  <div id=logoline>
    <div id=logo>
      <img src="https://www.gstatic.com/images/branding/product/1x/pagespeed_32dp.png"
           srcset="https://www.gstatic.com/images/branding/product/2x/pagespeed_32dp.png"
           width=32 height=32 alt="pagespeed logo">
    </div>
    <div id=logotext>PageSpeed</div>
  </div>
  <div id=navline>
    <a href="/doc/">&larr; documentation index</a>
  </div>
</div>

<div id=toc></div>