search

arduino / Arduino

Arduino IDE 1.x
https://www.arduino.cc/en/software
Other
14.11k stars 7k forks source link

Feature Request: Additional Library Manager URLs #6879

Open sleemanj opened 6 years ago

sleemanj commented 6 years ago

We do have Prefs : Additional Boards Manager URLs

We do not have Prefs : Additional LIbrary Manager URLs

Is there some objection to having Additional Library Manager URLs - or is it simply that it's not been implemented?

I searched the tickets for this but couldn't find anything, it seems like something that should already have at least been brought up as a natural adjunct to Board Manager URLs.

sleemanj commented 6 years ago

For reference, a quick skim of the code I expect the simplest thing from an implementation stand point would be here to run though a set consisting of the existing library_index.json / LIBRARY_INDEX_URL and any additional URLs and merge the responses into a single index to be written to the outputFile.

That way the only other change would be the actual addition of the field in preferences I expect, library manager etc wouldn't need to know it's index was sourced from multiple places.

May not be the best way from a philosophical standpoint though.