Skip to content

feat: toolchain management - #114

Open
robsimmons wants to merge 2 commits into
push-rtlptympkwvtfrom
manage-toolchain
Open

feat: toolchain management#114
robsimmons wants to merge 2 commits into
push-rtlptympkwvtfrom
manage-toolchain

Conversation

@robsimmons

@robsimmons robsimmons commented Sep 2, 2026

Copy link
Copy Markdown
Collaborator

Closes #25. Toolchains can be introduced with a second use of TrackedCommandForm, and modified with the same kind of inline modification form initially used for active editor sessions and duplicated for project templates

Selecting toolchain:
image

Downloading toolchain:
image

Removing toolchain (two-click confirmation)
image

@robsimmons
robsimmons force-pushed the manage-toolchain branch 2 times, most recently from b38f44e to 3da0762 Compare September 3, 2026 01:46
@robsimmons
robsimmons changed the base branch from main to push-rtlptympkwvt September 3, 2026 02:12
@robsimmons
robsimmons force-pushed the manage-toolchain branch 2 times, most recently from dae78ad to 61e3968 Compare September 3, 2026 16:01
@robsimmons
robsimmons force-pushed the manage-toolchain branch 2 times, most recently from 1cb006d to 2cc53b9 Compare September 5, 2026 02:09
robsimmons and others added 2 commits September 5, 2026 12:29
Toolchains can be introduced with a second use of TrackedCommandForm, and modified with the same kind of inline modification form initially used for active editor sessions and duplciated for project templates
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Admin UI for manipulating Lean toolchains

1 participant