elan icon indicating copy to clipboard operation
elan copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

Support for toolchain origins with underscores

Open mnixry opened this issue 4 months ago • 0 comments

related: #99

Currently, the remote toolchain reference feature on GitHub does not support repositories with underscores in their names. This limitation affects repositories like leanprover-community/mathematics_in_lean.

mnixry avatar Oct 15 '24 16:10 mnixry