Zulip Chat Archive
Stream: general
Topic: elan-cleanup
Jannis Limperg (Dec 03 2022 at 16:09):
My weekend project: a little script (written in Lean 4 of course) that cleans up unused toolchains in your .elan
directory. It detects used toolchains by looking for lean-toolchain
files below your home directory (excluding directories starting with .
), then deletes any toolchain not mentioned in a lean-toolchain
file.
At the moment there are very few bells and whistles (e.g. you can't customise where it looks for lean-toolchain
files), but maybe someone finds it useful nonetheless.
Matej Penciak (Dec 03 2022 at 19:37):
Works great! Thanks!
Last updated: Dec 20 2023 at 11:08 UTC