diff --git a/Makefile b/Makefile index ba21f1369426df1d8833b642428ed08428798919..503c3b09333789240d2c31df0c4d43182f2e2148 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