From d0a2d4ffe8c25326a5f27b5d77fabf98a0ee8580 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 19 Dec 2019 11:58:47 +0100
Subject: [PATCH] add 'macos-clean' target to Makefile to get rid of
 '.DS_Store' files

---
 scripts/Makefile.patch | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/scripts/Makefile.patch b/scripts/Makefile.patch
index e8472234d..f3e62f3cf 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 ###########################################################
  
-- 
GitLab