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.
---
 style.css | 17 -----------------
 1 file changed, 17 deletions(-)
 delete mode 100644 style.css

(limited to 'style.css')

diff --git a/style.css b/style.css
deleted file mode 100644
index 708d9aa..0000000
--- a/style.css
+++ /dev/null
@@ -1,17 +0,0 @@
-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