From 05a941f11e196b5661eb76ae06f467c725d1e64b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Franc=CC=A7ois=20Pottier?= <francois.pottier@inria.fr> Date: Tue, 11 Mar 2025 19:35:19 +0100 Subject: [PATCH] Makefile.monolith: remove [dune build @check]. This was useless and did not use the correct switch. --- Makefile.monolith | 1 - 1 file changed, 1 deletion(-) diff --git a/Makefile.monolith b/Makefile.monolith index f439892..2ccda1b 100644 --- a/Makefile.monolith +++ b/Makefile.monolith @@ -62,7 +62,6 @@ BUILD := $(shell \ .PHONY: all all: - @ $(DUNEBUILD) @check # build src/.merlin, etc. @(echo "(lang dune 2.0)" && \ echo "(context (opam (switch $(SWITCH))))" \ ) > dune-workspace.afl -- GitLab