Packages in GAP_PKGS_TO_CLONE aren't properly deleted before cloning:

[wilfwilson]

Let pkg be the variable containing an entry of the list GAP_PKGS_TO_CLONE.

Currently the script tries to delete existing versions of $pkg before trying to clone it, with this line:

pkg-ci-scripts/build_gap.sh

Line 50 in 3ce4725

rm -rf "$pkg"*

This works reasonably well if $pkg is simply the package name in lower case, e.g. digraphs or float.

It does not necessarily work so well if there is some capitalisation, such as Digraphs.

More importantly, if the format of $pkg is more complicated, i.e. digraphs/digraphs or https://github.com/digraphs/Digraphs then none of the existing versions get deleted.

This wastes time and may lead to the wrong version of the package being loaded.