add section at end for user's custom preferences

[berrythesoftwarecodeprogrammar]

proper section for users to append their own settings or to override settings in pyllyukko's user.js without having to go through and comment out things every time (im assuming entries with the same name which are later in the file can override settings above them. is that right? if not then oops, i guess it can still serve as a place for settings which arent in pyllyukko's user.js yet or wont ever be)

[pyllyukko]

without having to go through and comment out things every time

Good idea.

(im assuming entries with the same name which are later in the file can override settings above them. is that right?

Not sure.

i guess it can still serve as a place for settings which arent in pyllyukko's user.js yet or wont ever be

Yes and no. There might be problems when the user updates the user.js with git pull, as there will be conflicts. We should look into whether it's possible to include another file (e.g. user-custom.js) that the users can create on their own. That way there would be no conflicts with Git.

[berrythesoftwarecodeprogrammar]

ok i just confirmed that when there are multiple entries of the same name, the later ones override the ones before them. so any user differences could just be appended to the bottom and they will override your settings.
maybe there can be an extra file where users can add their custom preferences and then a script which is called after the git pull to append the users entries to user.js?

[pyllyukko]

Ok. Thanks for confirming this.

Appending stuff is not the problem, but the git pull will probably fail in the first place.

[berrythesoftwarecodeprogrammar]

oh right. yeah i just havent used it like that yet. i wonder what can be done

[pyllyukko]

We need to look into this. Many users probably has the need to customize stuff, so I think this is quite relevant.

[pyllyukko]

I'm unable to come up with any quick/easy/clean solution for this.

Maybe some Git hackery with customizations in it's own branch...? Dunno. Any suggestions? Because if the git pull fails, I think that's a real problem, as users are unable to update the user.js file.

[nodiscc]

When using another branch, you also sometimes have to resolve merge conflicts when merging pyllyukko's master branch into it. This is my current strategy, but it requires working with git mergetool, which might not be convenient for everyone.

Another possible strategy: let the user create his own custom.js, and run a Makefile that concatenates user.js and custom.js to a third file. The third file is the one that should be copied to user's profile.

[berrythesoftwarecodeprogrammar]

moved to #75