Commit 2024-09-03 09:13 ba7dc415

fix: do not get cache if Mathlib.Init is unavailable (#16437) You can see a few attempts and tests #16435: the final commits test what happens with and without cache for Mathlib.Init. Reported on Zulip