<div dir="ltr"><div class="gmail_extra">On Sun, Dec 23, 2012 at 8:55 PM, Barry Smith <span dir="ltr"><<a href="mailto:bsmith@mcs.anl.gov" target="_blank">bsmith@mcs.anl.gov</a>></span> wrote:<br><div class="gmail_quote">
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">   What do you mean? Do you mean manual1.ind?  Surely you don't mean from manual.pdf?</blockquote></div><br></div><div class="gmail_extra" style>
Yeah, we can grab it from manual1.ind and convert it to #page= links in the HTML man pages, which would render like<br><br>SNES<br><br>User's manual pages: 19, 29, 91, 98-105, ...</div><div class="gmail_extra" style><br>
</div><div class="gmail_extra" style>where each number is a #page= link.<br><br>Even better would be to somehow include the section name, maybe in the hover text, but I don't know a good way to get that information.</div>
</div>