genode/tool/depot
Martin Stein f6dd1f9b9c tool/depot: user-friendly error on missing port
In general, make the message conform to the according message of the
common build system. Adds instruction how to fix the missing/outdated
port.

Fixes #2573
2017-11-30 11:23:03 +01:00
..
mk tool/depot: user-friendly error on missing port 2017-11-30 11:23:03 +01:00
build depot: remove bin/<arch>/<api-version> subdir 2017-08-28 16:49:37 +02:00
create depot/create: build only if binaries are specified 2017-06-29 11:59:55 +02:00
dependencies Tool for assembling API/source/binary archives 2017-05-31 13:15:56 +02:00
download tool/depot: download archives from web server 2017-05-31 13:16:24 +02:00
extract Tool for assembling API/source/binary archives 2017-05-31 13:15:56 +02:00
publish tool/depot: download archives from web server 2017-05-31 13:16:24 +02:00