mccmcc@mastodon.socialOct 14, 2026, 10:27 PM@Andrev @dysfun Looking in ~/.local/bin, I see an "idris2" and a "pack".The bash installer for pack said only to delete ~/.local/pack . What is the correct uninstallation procedure for idris/pack? Is it documented somewhere?
gaytabasedysfun@treehouse.systemsOct 14, 2026, 10:29 PM@mcc @Andrev that is the documentation. and it evidently neglected to think about the pack config
Oct 14, 2026, 10:27 PM