Committed, thanks.

http://us2.php.net/manual/en/function.array-push.php says:



Note: If you use array_push() to add one element to the  array it's 
better to use $array[] = because in that  way there is no overhead of 
calling a function.



I'm not positive that it's applicable here since we're calling 
array(), but array() isn't a real function.



I only submitted this patch since it took 5 seconds and reduced a few 
lines of code that I had added.

Also, why are you optimizing this script? Does it really cause 
performance problems for you? Just thinking that optimization efforts 
could be better focused elsewhere...

Do you have any reference where this is explained? Or did you find 
this from your own benchmarks?

This removes array_push() calls from scripts/remove_prefs.php since 
that function can be slow.