make: add back tools cmd (#4281) · ffe5dff8d9 - tendermint - Gitea: Git with a cup of tea

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 <marbar3778@yahoo.com>

pull/4282/head

Marko 5 years ago

committed by

GitHub

parent

7d7b47a39a

commit

ffe5dff8d9

No known key found for this signature in database GPG Key ID: 4AEE18F83AFDEB23

1 changed files with 2 additions and 0 deletions

Unified View

							
								+ 2
								
								- 0
							
tools.mkView File
								
																@ -46,6 +46,8 @@ GOODMAN 			= $(TOOLS_DESTDIR)/goodman
															
																all: tools
																
																all: tools
															
																tools: certstrap protobuf goodman
															
																check: check_tools
																
																check: check_tools
															
																check_tools:
																
																check_tools: