Update all setting pull files

For convenience, python pull_files.py --all should really pull all files. Guys, please remember to add them to the list to avoid unwanted surprises! @tbevilac @cdaumann FYI