diff --git a/Makefile b/Makefile index 5bc8f472c95400efff461782caabc19914cf9445..a2bd02f45636a77e3971c40de345952b729337c5 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