Skip to content

Do not read a repeated tool name as an uninstalled one - #803

Merged
SimonCropp merged 1 commit into
mainfrom
fix-toolsorder-duplicate-throw
Aug 22, 2026
Merged

Do not read a repeated tool name as an uninstalled one#803
SimonCropp merged 1 commit into
mainfrom
fix-toolsorder-duplicate-throw

Commits

Commits on Aug 22, 2026