1 files changed, 23 insertions, 0 deletions
diff --git a/web-tools/web/_static/local/font.css b/web-tools/web/_static/local/font.css
new file mode 100644
index 0000000..4c9b109
--- /dev/null
+++ b/web-tools/web/_static/local/font.css
@@ -0,0 +1,23 @@
+a.a-hover-red {
+  color: inherit;
+}
+
+a.a-hover-red:hover {
+  color: #cc0000 !important;
+  text-decoration: none;
+}
+
+html,
+body,
+.tooltip,
+.popover {
+  font-family: 'DejaVuSans';
+}
+
+pre,
+code,
+kbd,
+samp,
+.text-monospace {
+  font-family: 'DejaVuSansMono';
+}