# HG changeset patch # User František Kučera # Date 1595780028 -7200 # Node ID 95add699346da668648790fa064c6450c318cf6b # Parent e2e36bc0a94c588b210a993f5779b02c9a827270 css: Latin Modern Sans + Latin Modern Mono (in ) + DejaVu Sans Mono (in
 due to box-drawing)

diff -r e2e36bc0a94c -r 95add699346d relpipe-data/css/DejaVuSansMono.woff
Binary file relpipe-data/css/DejaVuSansMono.woff has changed
diff -r e2e36bc0a94c -r 95add699346d relpipe-data/css/lmmono10-regular.woff
Binary file relpipe-data/css/lmmono10-regular.woff has changed
diff -r e2e36bc0a94c -r 95add699346d relpipe-data/css/lmsans10-regular.woff
Binary file relpipe-data/css/lmsans10-regular.woff has changed
diff -r e2e36bc0a94c -r 95add699346d relpipe-data/css/relpipe.css
--- a/relpipe-data/css/relpipe.css	Tue Jul 14 16:45:13 2020 +0200
+++ b/relpipe-data/css/relpipe.css	Sun Jul 26 18:13:48 2020 +0200
@@ -1,3 +1,33 @@
+@font-face {
+	font-family: "lmsans10-regular";
+	src: url("lmsans10-regular.woff");
+}
+
+@font-face {
+	font-family: "lmmono10-regular";
+	src: url("lmmono10-regular.woff");
+}
+
+@font-face {
+	font-family: "DejaVuSansMono";
+	src: url("DejaVuSansMono.woff");
+}
+
+body {
+	font-family: "lmsans10-regular", sans-serif;
+}
+
+code {
+	font-family: "lmmono10-regular", "DejaVuSansMono", monospace;
+}
+
+pre {
+	font-family: "DejaVuSansMono", monospace;
+	-moz-tab-size: 4;
+	-o-tab-size: 4;
+	tab-size: 4;
+}
+
 .logo {
 	background-color: black;
 	height: 64px;