# HG changeset patch
# User wenzelm
# Date 1604141940 -3600
# Node ID 8e9312e6a6d9d5a74b173235bb76950f9c3b8434
# Parent  0d3b623db61aa5f0c28eaf3f9e06afe9f9642da7
clarified generated settings;

diff -r 0d3b623db61a -r 8e9312e6a6d9 lib/Tools/components
--- a/lib/Tools/components	Sat Oct 31 11:50:09 2020 +0100
+++ b/lib/Tools/components	Sat Oct 31 11:59:00 2020 +0100
@@ -99,7 +99,11 @@
   else
     echo "Initializing \"$SETTINGS\""
     mkdir -p "$(dirname "$SETTINGS")"
-    echo "$SETTINGS_CONTENT" > "$SETTINGS"
+    {
+      echo "#-*- shell-script -*- :mode=shellscript:"
+      echo
+      echo "$SETTINGS_CONTENT"
+    } > "$SETTINGS"
   fi
 elif [ -n "$LIST_ONLY" ]; then
   echo