From e34f8ac7e65438f70a615585e97bd7f0889c49f9 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Wed, 11 Nov 2020 18:47:15 +0100 Subject: [PATCH] fix find in clean --- Makefile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 9f262326d..ac8dba01d 100644 --- a/Makefile +++ b/Makefile @@ -15,7 +15,8 @@ phony: ; clean: Makefile.coq +@$(MAKE) -f Makefile.coq clean - find theories tests exercises solutions \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true + @# Make sure not to enter the `_opam` folder. + find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true rm -f Makefile.coq .lia.cache builddep/* .PHONY: clean -- GitLab