From 13da50ea801e38b275eafdb53212a8c62353ba5f Mon Sep 17 00:00:00 2001
From: Jakob Yanagibashi <jakob.yanagibashi@rwth-aachen.de>
Date: Tue, 9 May 2023 22:02:02 +0000
Subject: [PATCH] Use Roboto Mono font
---
css/main.css | 2 +-
index.html | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/css/main.css b/css/main.css
index a5f149c..bd6e715 100644
--- a/css/main.css
+++ b/css/main.css
@@ -12,7 +12,7 @@
body {
display: flex;
flex-flow: column wrap;
- font-family: "Space Mono", ui-monospace, monospace, ui-sans-serif, sans-serif;
+ font-family: "Roboto Mono", ui-monospace, monospace, ui-sans-serif, sans-serif;
-webkit-user-select: none; /* still needed for Safari 16 */
user-select: none;
}
diff --git a/index.html b/index.html
index e1c70ad..9b64b8e 100644
--- a/index.html
+++ b/index.html
@@ -16,7 +16,7 @@
<link rel="preconnect" href="https://fonts.googleapis.com" />
<link rel="preconnect" href="https://fonts.gstatic.com" crossorigin />
<link
- href="https://fonts.googleapis.com/css2?family=Space+Mono&display=swap"
+ href="https://fonts.googleapis.com/css2?family=Roboto+Mono&display=swap"
rel="stylesheet"
/>
</head>
--
GitLab