digraphs
Keep `digraphs-lib-x.y.tar.gz` somewhere other than in the actual repo
It's quite a big blob (currently 35MB) that, since it is a compressed .tar.gz archive, is an essentially completely different file with each minor change. I don't think it's really appropriate to increase the size of this repo by 35MB each time we tweak the digraphs-lib. If there's some sensible way that we could host it elsewhere, I think that would be better.
Is there perhaps some GitHub facility available for such things?
Obviously this isn't a very serious issue.
cf. #826.
Alternatively, perhaps digraphs-lib could be its own repository in the digraphs organisation, and digraphs-lib-0.7.tar.gz could actually be the v0.7 release archive on GitHub? This would save a lot of space because the repo would only have to contain the individual compressed digraph files, which would presumably never change between versions; the digraphs-lib-x.y.tar.gz files would never have to exist in the repository, they would just be part of the GitHub release system.
I've started work on this https://github.com/digraphs/digraphs-lib. Anyone is welcome to contribute to it.
The CI could just clone this repo rather than having to deal with finding the latest tarball and unpacking it.