1 files changed, 1 insertions, 0 deletions

diff --git a/Makefile b/Makefile
index 5a6a1005ee..32de1f46bf 100644
--- a/Makefile
+++ b/Makefile
@@ -743,6 +743,7 @@ clean:: archclean
 	rm -f tools/*.cm[io]
 	rm -f scripts/*.cm[io]
 	rm -f dev/*.cm[io]
+	rm -f */*.pp[iox] contrib/*/*.pp[iox]
 
 cleanconfig::
 	rm -f config/Makefile config/coq_config.ml