In article <[EMAIL PROTECTED]>,
Duane Clark <[EMAIL PROTECTED]> wrote:
>At least in Linux, create a file called user.js (in the same place as
>pref.js) and put your customizations there. Mozilla will still use them
>(it copies them to pref.js), but this will prevent Mozilla from undoing
>them. Just realize that deleting a pref from user.js will not delete it
>from pref.js.
I already had
user_pref("font.minimum-size.x-western", 11);
in my user.js but that gets stored now as
user_pref("font.minimum-size.x-western", "11");
in prefs.js on exit. The next mozilla run then seems to take the "11"
value from prefs.js instead of the 11 (without quotes) from user.js so
my font sizes are wrong. So this doesn't work either :-(.
Arjan
