From a069fdf9804ef369392f308ed2159f62b564911a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Franc=CC=A7ois=20Pottier?= <francois.pottier@inria.fr> Date: Thu, 31 Dec 2020 10:40:36 +0100 Subject: [PATCH] Fix [make install]. --- Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/Makefile b/Makefile index a5185fc..0c10fc3 100644 --- a/Makefile +++ b/Makefile @@ -21,6 +21,7 @@ all: .PHONY: install install: + dune build -p $(THIS) dune install -p $(THIS) .PHONY: clean -- GitLab