On Sun, Jan 10, 2021 at 9:46 AM Vincent Legoll wrote: > * I've not checked the difference size (nor that it matters) between zip > and tar.gz, you may want to use the smallest one to minimize download. > I just did, and the tgz wins: 3.1 MB vs 5.7 MB -- Vincent Legoll