From b604c3badfd4e6280ac6a3843b0d4a0643601522 Mon Sep 17 00:00:00 2001 From: John David Pressman Date: Sat, 1 Jun 2019 02:06:44 -0700 Subject: [PATCH] Undo addition of source command to makefile build-deps --- makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/makefile b/makefile index 675e82ad8..e775b0376 100644 --- a/makefile +++ b/makefile @@ -5,7 +5,7 @@ build-deps: ./build-deps.sh build: build-deps - source ./build.sh + ./build.sh test: build dune build @ligo-test