From 5ec43446818fbf7e4eb7f34735cf12bc0611495c Mon Sep 17 00:00:00 2001
From: Daniel Arndt <daniel.arndt@iwr.uni-heidelberg.de>
Date: Sun, 22 Jul 2018 18:35:17 +0200
Subject: [PATCH] Ignore deleted files when formatting

---
 contrib/utilities/indent_common.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/contrib/utilities/indent_common.sh b/contrib/utilities/indent_common.sh
index f8169780c8..6bbeb92115 100644
--- a/contrib/utilities/indent_common.sh
+++ b/contrib/utilities/indent_common.sh
@@ -247,7 +247,7 @@ process_changed()
   esac
 
   ( git ls-files --others --exclude-standard -- ${1};
-    git diff --name-only $COMMON_ANCESTOR_WITH_MASTER -- ${1} )|
+    git diff --name-only --diff-filter=d $COMMON_ANCESTOR_WITH_MASTER -- ${1} )|
       sort -u |
       grep -E "^${2}$" |
       ${XARGS} '\n' -n 1 -P 10 -I {} bash -c "${3} {}"
-- 
2.39.5