From 6483721f9858226a9ecfd3c3062662339e6c2906 Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.maroneze@cea.fr> Date: Fri, 16 Jul 2021 18:29:10 +0200 Subject: [PATCH] [Makefile] fix clean rule under Windows --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 5bc8f472c95..a2bd02f4563 100644 --- a/Makefile +++ b/Makefile @@ -2133,7 +2133,7 @@ else endif hdrck-clean: - $(RM) headers/hdrck headers/hdrck.o + $(RM) $(HDRCK) headers/hdrck.o $(RM) headers/hdrck.cmx headers/hdrck.cmi headers/hdrck.cmp clean:: hdrck-clean -- GitLab