Index

[andrejbauer]

Are we going to have an index of terms? Even though it is easy to search through a PDF file, an index still points the reader to the most relevant place where a given term is discussed.

[mikeshulman]

I think that's a good idea, but is it yet time to worry about it?

[RobertHarper]

do it last, the process is tedious and error-prone, and, contrary to what you may think, it cannot be done mechanically.

bob

Sent from tablet

On Mar 7, 2013, at 12:06, Mike Shulman notifications@github.com wrote:

I think that's a good idea, but is it yet time to worry about it?

—
Reply to this email directly or view it on GitHub.

[andrejbauer]

I agree it should be done in the end. It's not that much work, I did it for my thesis (250 pages) in two days.