doc: shrink font sizes in navbar
authorRamprasad Venkataraman <ramv@illinois.edu>
Sat, 4 Aug 2012 16:39:36 +0000 (11:39 -0500)
committerRamprasad Venkataraman <ramv@illinois.edu>
Sat, 4 Aug 2012 16:39:36 +0000 (11:39 -0500)
commit6eeccd894e81b998b5093455d2b3b1f1b030a122
tree9d1c661bfc150700ec2f69fafe0445180d563857
parentd63c610db5091ff7751c96a13ccef8be0d96b7e0
doc: shrink font sizes in navbar
doc/dot.latex2html-init
doc/manual.css