clarified generated settings;
authorwenzelm
Sat, 31 Oct 2020 11:59:00 +0100
changeset 72524 8e9312e6a6d9
parent 72523 0d3b623db61a
child 72525 8eb0b663fa20
clarified generated settings;
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