Skip to content

Conversation

@eric-wieser
Copy link

@eric-wieser eric-wieser commented Feb 14, 2025

This was legal (accidentally?) in previous elan version, and let me smuggle Bazel labels into the lean-toolchain files.

Look, my setup works for me. Just add an option to reenable ...

Fixes #139

This was legal (accidentally?) in previous elan version, and let me smuggle Bazel target names into the `lean-toolchain` files.

https://xkcd.com/1172 obvious applies here.
@Kha
Copy link
Member

Kha commented Feb 27, 2025

I can't accept this if it just throws away parts of the regex match. But for local toolchains, even the version match doesn't make much sense. How about changing the code so that we simply accept name as-is as a local toolchain if it exists and only do the matching otherwise?

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.

elan toolchain list refuses to list any toolchains

2 participants