1
0
mirror of https://github.com/RIOT-OS/RIOT.git synced 2024-12-29 04:50:03 +01:00

dist/tools/desvirt: use RIOTTOOLS variable

This commit is contained in:
Gaëtan Harter 2018-03-22 17:21:41 +01:00
parent 98d33a5eca
commit 297ca898fe
No known key found for this signature in database
GPG Key ID: 76DF6BCF1B1F883B

View File

@ -1,7 +1,7 @@
TOOL_NAME=desvirt
TOOL_URL=https://github.com/des-testbed/desvirt.git
TOOL_VERSION=master
TOOL_DIR=$(RIOTBASE)/dist/tools/$(TOOL_NAME)/$(TOOL_NAME)
TOOL_DIR=$(RIOTTOOLS)/$(TOOL_NAME)/$(TOOL_NAME)
.PHONY: desvirt-check desvirt-check-topo-file desvirt-check-topo-args desvirt-clean \
desvirt-distclean desvirt-define desvirt-undefine desvirt-start desvirt-stop desvirt-list