From 46969672f55eca83db18cde476a2cccbb74a1718 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Franc=CC=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Thu, 6 Jan 2022 19:10:11 +0100
Subject: [PATCH] Temporarily remove the call to [make merlin], because it
 fails. (Recent versions of Dune do not generate src/.merlin any more.)
 Waiting for a better patch.

---
 Makefile | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Makefile b/Makefile
index 096220f..da8bf42 100644
--- a/Makefile
+++ b/Makefile
@@ -38,9 +38,7 @@ TARGETS  := src fuzz benchmark
 
 .PHONY: all
 all:
-	@ dune build $(PROFILE) $(TARGETS) ; make merlin
-# Regardless of whether compilation succeeds or fails,
-# invoke [make merlin] to patch src/.merlin.
+	@ dune build $(PROFILE) $(TARGETS)
 
 # [make setup] installs the packages that we need in whatever opam
 # switch is currently active.
@@ -52,6 +50,7 @@ setup:
 
 .PHONY: merlin
 merlin:
+	@ touch src/.merlin
 # Add a preprocessing directive at the end of the FLG line.
 	@ sed -i.bak '/^FLG/ s/$$/ -pp "cppo -D dev"/' src/.merlin
 	@ rm -f src/.merlin.bak
-- 
GitLab