From b1c687faac22eaea466bef4cd87fd8dc8aa32b7a Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 16 Feb 2019 16:55:59 -0600 Subject: [PATCH] chore: make default target `build`, not `dev` --- Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index b24f052f..a8967cda 100644 --- a/Makefile +++ b/Makefile @@ -12,11 +12,11 @@ OPTS= -j $(J) LIB=$(addprefix $(NAME), .cma .cmxa .cmxs) -dev: build-dev test - build: @dune build $(OPTS) @install --profile=release +dev: build-dev test + build-dev: @dune build $(OPTS) @install