From: Matthias Maier <tamiko@43-1.org>
Date: Tue, 11 Feb 2020 17:15:44 +0000 (-0600)
Subject: Indent script: Do not use --diff-filter=d
X-Git-Tag: v9.2.0-rc1~523^2
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=ac0f23f2826e9ff1fc8afa18fde5297bc95f6d25;p=dealii.git

Indent script: Do not use --diff-filter=d

This hopefully fixes some compatibility issues with ancient git versions
not supporting the --diff-filter option.

Closes #9489
---

diff --git a/contrib/utilities/indent_common.sh b/contrib/utilities/indent_common.sh
index 57c5c0d9b0..aeca8a4fe0 100644
--- a/contrib/utilities/indent_common.sh
+++ b/contrib/utilities/indent_common.sh
@@ -307,8 +307,9 @@ process_changed()
   esac
 
   ( git ls-files --others --exclude-standard -- ${1};
-    git diff --name-only --diff-filter=d $COMMON_ANCESTOR_WITH_MASTER -- ${1} )|
+    git diff --name-only $COMMON_ANCESTOR_WITH_MASTER -- ${1} )|
       sort -u |
+      xargs -n 1 ls -d 2>/dev/null |
       grep -E "^${2}$" |
       ${XARGS} '\n' -n 1 -P 10 -I {} bash -c "${3} {}"
 }