increase font size in symbol index #417

Open
awodey opened this Issue Jul 14, 2013 · 1 comment

Projects

None yet

2 participants

@awodey
Contributor
awodey commented Jul 14, 2013

against my own prior opinion, I think the font size in the symbol index should be increased to the match the main text, rather than the index. The reason is that symbols often involve (possibly iterated) sub- and superscripts, which get too small to read comfortably (at least for old eyes ...).

@cangiuli
Contributor

I tried it out; it causes a bunch of the descriptions to wrap onto a second line, but otherwise looks fine, and doesn't actually change the page count of hott-ustrade. Do we still want this?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment