# 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