From e40d0e3f82c3d00d27749f4bf3bd2eaefc61eec7 Mon Sep 17 00:00:00 2001
From: Arun Isaac
Date: Sat, 19 Jun 2021 16:04:26 +0530
Subject: website: Move CSS into the website directory.

That way, there is no need to copy it when building the website.

* Makefile.am (website/style.css): Delete target.
(website): Do not depend on the website/style.css target.
(clean-local): Clean up only website/index.html and
website/manual/dev/en, not the entire website directory.
* style.css: Move to website/style.css.
---
 website/style.css | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 website/style.css

(limited to 'website')

diff --git a/website/style.css b/website/style.css
new file mode 100644
index 0000000..708d9aa
--- /dev/null
+++ b/website/style.css
@@ -0,0 +1,17 @@
+body {
+    margin: 40px auto;
+    max-width: 900px;
+    line-height: 1.6;
+    font-size: 18px;
+    color: #444;
+    padding: 0 10px;
+}
+
+h1, h2, h3 {
+    line-height: 1.2;
+}
+
+/* Make the svg badges clickable. */
+object {
+    pointer-events: none;
+}
-- 
cgit v1.2.3