diff --git a/tools/purge-github-cache.sh b/tools/purge-github-cache.sh new file mode 100755 index 000000000..01fdb2fed --- /dev/null +++ b/tools/purge-github-cache.sh @@ -0,0 +1,6 @@ +#!/bin/bash -ex + +# This script assumes that the Github CLI is installed and that +# the authenticated user has appropriate authorization. + +gh cache delete --all \ No newline at end of file