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.

1 files changed, 3 insertions, 3 deletions

diff --git a/doc_src/user_doc.css b/doc_src/user_doc.css
index 5c041fd3..b290bee9 100644
--- a/doc_src/user_doc.css
+++ b/doc_src/user_doc.css
@@ -21,7 +21,7 @@ body {
 }
 /*Top site index*/
 .qindex {
-    font: 500 1.4rem/3.6rem DejaVuSansCondensed, DejaVuSans, Roboto, "Lucida Grande", Calibri, Verdana, "Helvetica Neue", Helvetica, Arial, sans-serif;
+    font: 500 1.4rem/3.6rem DejaVuSans, Roboto, "Lucida Grande", Calibri, Verdana, "Helvetica Neue", Helvetica, Arial, sans-serif;
     border: none;
     color: white;
     text-align: center;
@@ -48,7 +48,7 @@ body {
 .fish_left_bar {
     width: 25rem;
     color: white;
-    font-family: DejaVuSansCondensed, DejaVuSans, Roboto, "Lucida Grande", Calibri, Verdana, "Helvetica Neue", Helvetica, Arial, sans-serif;
+    font-family: DejaVuSans, Roboto, "Lucida Grande", Calibri, Verdana, "Helvetica Neue", Helvetica, Arial, sans-serif;
     background-color: #1f2d53;
 }
 .fish_right_bar {
@@ -101,7 +101,7 @@ a { color: #3d5cb3; }
 p { margin: 1rem 0; }
 h1, h2, h3, h4, h5, h6 {
     color: #1f2d53;
-    font-family: DejaVuSansCondensed-Bold, DejaVuSans, Roboto, "Lucida Grande", Calibri, Verdana, sans-serif;
+    font-family: DejaVuSans, Roboto, "Lucida Grande", Calibri, Verdana, sans-serif;
 }
 h1 {
     margin: 1.6rem 0 1rem 0;