Tuned

2022-12-01 14:22:32 +01:00 · 2022-12-01 14:22:32 +01:00 · 09e9980691
parent 94ce3fdec2
commit 09e9980691
1 changed files with 1 additions and 2 deletions
--- 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"