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;