From 4d130cefeeca99ab0f66cdb8df4c50a28ed18cd8 Mon Sep 17 00:00:00 2001
From: Andre Noll <maan@tuebingen.mpg.de>
Date: Wed, 8 May 2024 02:21:37 +0200
Subject: [PATCH] index.html: Remove navigation menu.

The page has become simple enough, making the navigation links useless.
The page no longer contains any <hr> tags, so remove the corresponding
part of the style sheet.
---
 index.html.m4 | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/index.html.m4 b/index.html.m4
index 34e4b74..2a55e34 100644
--- a/index.html.m4
+++ b/index.html.m4
@@ -10,11 +10,6 @@ dnl SPDX-License-Identifier: GPL-2.0
 			background-color: #ffffff;
 			color: #333333;
 		}
-
-		hr {
-			background-color: #ffff00;
-		}
-
 		a {
 			color: #4444ff;
 		}
@@ -33,10 +28,6 @@ dnl SPDX-License-Identifier: GPL-2.0
 			</td>
 		</tr>
 	</table>
-	<hr>
-	[<a href="`#'installation">Installation</a>]
-	[<a href="`#'resources">Resources</a>]
-	<hr>
 
 	<p> DESCRIPTION1() </p>
 	<p> DESCRIPTION2() </p>
-- 
2.39.5