Commit 2026-04-12 01:02 be3aab41

feat: cache only emits a warning when Git is not found (#37847) Currently lake exe cache get requires git to be installed, and that the current folder is a git repo. Sometimes this is annoying:

• someone sends a ZIP without .git subfolder,
• someone uploads supplementary material of a publication without .git subfolder
• probably annoying for a trylean bundle This PR downgrades the currently emitted errors to warnings, and continues to fetch from the leanprover-community/mathlib4 cache only in case any of these warnings is triggered.