1 files changed, 33 insertions, 0 deletions

diff --git a/web/input/resources/plugins.css b/web/input/resources/plugins.css
index c9b31a3..872283e 100644
--- a/web/input/resources/plugins.css
+++ b/web/input/resources/plugins.css
@@ -145,3 +145,36 @@ p#news-footer {
     text-align: center;
     font-size: small;
 }
+
+/*
+ * On narrow displays, replace the menu bar with a simple list of items, and
+ * omit the GitHub ribbon.
+ */
+
+@media (max-width: 45em) {
+    div#menu {
+        padding: 1em;
+        background-color: #fff;
+        border-bottom: 1px dotted #696969;
+    }
+
+    div#menu span {
+        display: list-item;
+        padding: 0;
+    }
+
+    div#menu span#current {
+        color: #5a95c7;
+        background-color: #fff;
+    }
+
+    div#menu a {
+        color: #1b476b;
+    }
+}
+
+@media (max-width: 60em) {
+    div#github-ribbon {
+        display: none;
+    }
+}