Don't use DejaVu Sans Condensed for documentation rendering.

This font, at least under Kubuntu 14.04 and Firefox I use is rather
ugly. Anti-aliasing is wrong, and the spaces between letters are
rather random. It makes reading the documentation headings and table
of contents harder than it needs to be.

Those issues don't happen with DejaVu Sans.