From d64ab1d1436d866e37163b68e73d2b040cee980c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Wed, 18 Dec 2019 02:30:17 +0100
Subject: [PATCH] add 'make vacuum' target to get rid of stale build files

---
 scripts/Makefile.patch | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/scripts/Makefile.patch b/scripts/Makefile.patch
index 76a5ace74..e8472234d 100644
--- a/scripts/Makefile.patch
+++ b/scripts/Makefile.patch
@@ -29,3 +29,14 @@
  # FIXME: not quite right, since the output name is different
  gallinahtml: GAL=-g
  gallinahtml: html
+@@ -587,6 +593,10 @@
+ 	$(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx)
+ .PHONY: archclean
+ 
++vacuum:: cleanall
++	$(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
+ 
+ # Compilation rules ###########################################################
+ 
-- 
GitLab