Scalable font size in code highlighter

quadroid · Jan 15, 2022 · d641d15 · d641d15
1 parent eee92bf
commit d641d15
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/kb/css/sh.css b/kb/css/sh.css
@@ -2,7 +2,7 @@
 .dp-highlighter
 {
 	font-family: Consolas, Menlo, Monaco, "Courier New", Courier, monospace;
-	font-size: 12px;
+	font-size: .95em;
 	background-color: #efeee8;
 	width: 100%;
 	overflow: auto;
@@ -110,7 +110,7 @@
 .dp-highlighter .tools
 {
 	padding: 3px 8px 3px 10px;
-	font: 9px Verdana, Geneva, Arial, Helvetica, sans-serif;
+	font-family: Verdana, Helvetica, 'Helvetica Neue', Arial, sans-serif;
 	color: silver;
 	background-color: #f8f8f8;
 	padding-bottom: 10px;
@@ -126,7 +126,7 @@
 }
 .dp-highlighter .tools a
 {
-	font-size: 9px;
+	font-size: 80%;
 	color: #a0a0a0;
 	background-color: inherit;
 	text-decoration: none;