Add an install target in Makefile

math-comp · Jan 24, 2023 · 759179e · 759179e
1 parent ce1bdcf
commit 759179e
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/Makefile b/Makefile
@@ -12,5 +12,8 @@ default: build
 build:
 	$(DUNE) build
 
+install:
+	$(DUNE) install
+
 clean:
 	$(DUNE) clean