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
create
dependencies
download
extract
publish