diff options
Diffstat (limited to 'config/Config-devel.in')
| -rw-r--r-- | config/Config-devel.in | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/config/Config-devel.in b/config/Config-devel.in index 3f73cb404d..e16e6ecaab 100644 --- a/config/Config-devel.in +++ b/config/Config-devel.in @@ -17,6 +17,20 @@ menuconfig DEVEL Store built firmware images and filesystem images in this directory. If not set, uses './bin/$(BOARD)' + config DOWNLOAD_TOOL_CUSTOM + string "Use custom download tool" if DEVEL + default "" + help + Use and force custom download tool instead of relying on autoselection + between curl if available and wget as a fallback. + + download.pl supports 3 tools officially aria2c, curl and wget. + If one of the tool is used in this config, download.pl will use the + default args to make use of them. + + If the provided string is different than aria2c, curl or wget, the command + is used as is and the download url will be appended at the end of such command. + config DOWNLOAD_FOLDER string "Download folder" if DEVEL default "" |