Problem when adding a custom board in board manager

[adrivin]

Hi @ptillisch

Thank you a lot !

I tried your first solution and it works !

I will try the second one now so that the user will not need to manually install the tool.