aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile2
1 files changed, 2 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 7aadc0a08f..09bd30186c 100644
--- a/Makefile
+++ b/Makefile
@@ -1120,6 +1120,7 @@ archclean::
rm -f toplevel/*.cmx toplevel/*.[so]
rm -f ide/*.cmx ide/*.[so]
rm -f ide/utils/*.cmx ide/utils/*.[so]
+ rm -f translate/*.cmx translate/*.[so]
rm -f tools/*.cmx tools/*.[so]
rm -f scripts/*.cmx scripts/*.[so]
rm -f dev/*.cmx dev/*.[so]
@@ -1139,6 +1140,7 @@ clean:: archclean
rm -f toplevel/*.cm[io]
rm -f ide/*.cm[io]
rm -f ide/utils/*.cm[io]
+ rm -f translate/*.cm[io]
rm -f tools/*.cm[io]
rm -f scripts/*.cm[io]
rm -f dev/*.cm[io]