From a875e64571d377b5c54da2b2ac31393bbb402341 Mon Sep 17 00:00:00 2001 From: David Allsopp Date: Thu, 6 Dec 2018 18:14:38 +0000 Subject: [PATCH] Missing clean items from GPR#1063 --- Makefile | 1 + otherlibs/dynlink/Makefile | 3 ++- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index a3fb1d7e0..fd7f11f5f 100644 --- a/Makefile +++ b/Makefile @@ -1274,6 +1274,7 @@ partialclean:: rm -f driver/compdynlink.mlopt rm -f driver/compdynlink.mli rm -f driver/compdynlink_platform_intf.ml + rm -f driver/compdynlink_platform_intf.mli rm -f driver/compdynlink_common.ml rm -f driver/compdynlink_common.mli rm -f driver/compdynlink_types.mli diff --git a/otherlibs/dynlink/Makefile b/otherlibs/dynlink/Makefile index 8a5e0ee3d..52aa55b4e 100644 --- a/otherlibs/dynlink/Makefile +++ b/otherlibs/dynlink/Makefile @@ -164,6 +164,7 @@ partialclean: rm -f extract_crc *.cm[ioaxt] *.cmti *.cmxa clean: partialclean - rm -f *.$(A) *.$(O) *.so *.dll dynlink.mlopt + rm -f *.$(A) *.$(O) *.so *.dll dynlink.mlopt \ + dynlink_platform_intf.mli depend: