From 09e9980691c135ca9cadab97b710445ca2110cad Mon Sep 17 00:00:00 2001
From: Makarius <makarius@sketis.net>
Date: Thu, 1 Dec 2022 14:22:32 +0100
Subject: [PATCH] Tuned

---
 etc/settings | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/etc/settings b/etc/settings
index dcc1a87b..5c450b81 100644
--- a/etc/settings
+++ b/etc/settings
@@ -1,5 +1,4 @@
 # -*- shell-script -*- :mode=shellscript:
 
 ISABELLE_DOF_HOME="$COMPONENT"
-ISABELLE_DOCS="$ISABELLE_DOF_HOME/doc":"$ISABELLE_DOCS"
-
+ISABELLE_DOCS="$ISABELLE_DOF_HOME/doc:$ISABELLE_DOCS"