From ffe5dff8d987f33cfb65e0b4d024406444cf7f3f Mon Sep 17 00:00:00 2001 From: Marko Date: Thu, 2 Jan 2020 20:48:01 +0100 Subject: [PATCH] make: add back tools cmd (#4281) previous PR seems to have deleted the tools cmd, this adds it back in Signed-off-by: Marko Baricevic --- tools.mk | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tools.mk b/tools.mk index fcf3549e2..140bcfd3e 100644 --- a/tools.mk +++ b/tools.mk @@ -46,6 +46,8 @@ GOODMAN = $(TOOLS_DESTDIR)/goodman all: tools +tools: certstrap protobuf goodman + check: check_tools check_tools: