From f0619a16990916bbea2358b11caaa8221e57482d Mon Sep 17 00:00:00 2001
From: Dmytro Meleshko <dmytro.meleshko@gmail.com>
Date: Sat, 9 Jan 2021 20:44:38 +0200
Subject: [PATCH] [mozilla] add a little Firefox devtools customization

---
 mozilla/firefox/userContent.css | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 mozilla/firefox/userContent.css

diff --git a/mozilla/firefox/userContent.css b/mozilla/firefox/userContent.css
new file mode 100644
index 0000000..932f3e5
--- /dev/null
+++ b/mozilla/firefox/userContent.css
@@ -0,0 +1,14 @@
+/* prettier-ignore */
+@-moz-document url-prefix(chrome://devtools/content/), url(about:devtools-toolbox) {
+  :root {
+    --theme-body-font-size: 13px !important;
+    --theme-code-font-size: 13px !important;
+    --theme-code-line-height: calc(15 / 13) !important;
+  }
+
+  /*
+  :root[platform="linux"] {
+    --monospace-font-family: "Ubuntu Mono" !important;
+  }
+  */
+}