Style: Remove font fallback to Helvetica, Arial

These fonts are not common nowadays and do not look native.

Let the user agent set the fallback font in the rare cases the
distributed font cannot be used (eg. missing on server or unsupported by
client).

Author: Julow

src/html_support_files/odoc.css

@@ -282,7 +282,7 @@ header {
 }
 
 nav {
-  font-family: "Fira Sans", Helvetica, Arial, sans-serif;
+  font-family: "Fira Sans", sans-serif;
 }
 
 /* Basic markup elements */
@@ -413,7 +413,7 @@ a.anchor {
 a.source_link {
   float: right;
   color: var(--source-color);
-  font-family: "Fira Sans", Helvetica, Arial, sans-serif;
+  font-family: "Fira Sans", sans-serif;
   font-size: initial;
 }
 
@@ -422,7 +422,7 @@ a.source_link {
    we restart the sequence there like h2  */
 
 h1, h2, h3, h4, h5, h6, .h7, .h8, .h9, .h10 {
-  font-family: "Fira Sans", Helvetica, Arial, sans-serif;
+  font-family: "Fira Sans", sans-serif;
   font-weight: 400;
   padding-top: 0.1em;
   line-height: 1.2;