mirror of
https://github.com/mmueller41/genode.git
synced 2026-01-21 12:32:56 +01:00
By replacing the formerly hard-coded $(GENODE_DIR)/tool/depot/ by the variable DEPOT_TOOL_DIR, the depot tools can be hosted outside the Genode source tree, i.e., as part of the Goa tool.