From 9ca7a5d7f8625e821deba7b2da9ec37249af14e4 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 30 Jul 2021 11:23:14 +0200
Subject: [PATCH] [Makefile] remove generated binaries when distcleaning

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index ba21f136942..503c3b09333 100644
--- a/Makefile
+++ b/Makefile
@@ -2339,7 +2339,7 @@ dist-clean distclean: clean clean-doc \
 	$(RM) src/dummy/*/*.cm* src/dummy/*/*.o src/dummy/*/*.a \
 		src/dummy/*/*.annot src/dummy/*/*~ src/dummy/*/*.output \
 		src/dummy/*/*.annot src/dummy/*/\#*
-
+	$(RM) $(CHECK_NEWLINES) $(ISUTF8)
 
 ifeq ($(OCAMLWIN32),yes)
 # Use Win32 typical resources
-- 
GitLab