diff --git a/scripts/Makefile.patch b/scripts/Makefile.patch index e8472234d4bd81b9e1658c3b1fb21e304031796c..f3e62f3cfa2348b573ca14511d96b490167eb76a 100644 --- a/scripts/Makefile.patch +++ b/scripts/Makefile.patch @@ -29,7 +29,7 @@ # FIXME: not quite right, since the output name is different gallinahtml: GAL=-g gallinahtml: html -@@ -587,6 +593,10 @@ +@@ -585,6 +591,14 @@ $(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx) .PHONY: archclean @@ -37,6 +37,10 @@ + $(SHOW)'VACUUMING *.vo *.glob .*.aux <empty directories>' + $(HIDE)find . -depth \( -iname '*.vo' -or -iname '*.glob' -or -iname '.*.aux' \) ! -path './.git/*' -delete + $(HIDE)find . -depth -type d -empty ! -path './.git/*' -delete ++ ++macos-clean:: ++ $(SHOW)'CLEAN .DS_Store' ++ $(HIDE)find . -depth -iname '.DS_Store' ! -path './.git/*' -delete # Compilation rules ###########################################################