diff --git a/etc/settings b/etc/settings index dcc1a87..5c450b8 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"