From c584eab2e92435566b5a72bdc75a47e3cd98d6a7 Mon Sep 17 00:00:00 2001
From: Alex Cabal <alex@alexcabal.com>
Date: Sun, 13 Sep 2020 19:22:50 -0500
Subject: [PATCH] In the manual, update dot leaders to be larger dots instead
 of dashes

---
 www/css/manual.css | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/www/css/manual.css b/www/css/manual.css
index 21700aea..e1df54f1 100644
--- a/www/css/manual.css
+++ b/www/css/manual.css
@@ -404,7 +404,7 @@ figure.corrected code{
 .manual > article > section > section[id] section > aside.number::after{
 	content: " ";
 	width: 2rem;
-	border-bottom: 1px dashed;
+	border-bottom: 2px dotted;
 	border-color: rgba(0, 0, 0, .5);
 	display: block;
 	margin-left: 10.25rem;