Commit 2023-01-10 18:51 1d47ea1b
View on Github →feat: specific file names for cache get and cache get! (#1430)
This PR allows arguments for cache get and cache get! as explained in the help menu:
'get' and 'get!' can process list of paths, allowing the user to be more
specific about what should be downloaded. For example, with automatic glob
expansion in shell, one can call:
$ lake exe cache get Mathlib/Algebra/Field/* Mathlib/Data/*
Which will download the cache for:
* Everything that starts with 'Mathlib/Algebra/Field/'
* Everything that starts with 'Mathlib/Data/'
* Everything that's needed for the above