From c0644789c206825b4b73792709d5d4d76e019d6d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Franc=CC=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Wed, 7 Aug 2024 21:22:52 +0200
Subject: [PATCH] Fix [make install].

---
 Makefile | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index 6454e45..696c848 100644
--- a/Makefile
+++ b/Makefile
@@ -64,7 +64,9 @@ versions:
 	@ dune build --workspace dune-workspace.versions -p $(THIS)
 
 .PHONY: install
-install: all
+install:
+	@ dune clean
+	@ dune build -p $(THIS)
 	@ dune install -p $(THIS)
 
 .PHONY: clean
-- 
GitLab