]> https://gitweb.dealii.org/ - dealii.git/commitdiff
Ignore deleted files when formatting 6953/head
authorDaniel Arndt <daniel.arndt@iwr.uni-heidelberg.de>
Sun, 22 Jul 2018 16:35:17 +0000 (18:35 +0200)
committerDaniel Arndt <daniel.arndt@iwr.uni-heidelberg.de>
Sun, 22 Jul 2018 16:35:17 +0000 (18:35 +0200)
contrib/utilities/indent_common.sh

index f8169780c8675398d1bd520fa2509a582510d671..6bbeb92115abb20494d4d60885b4dbf64d17903d 100644 (file)
@@ -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} {}"

In the beginning the Universe was created. This has made a lot of people very angry and has been widely regarded as a bad move.

Douglas Adams


Typeset in Trocchi and Trocchi Bold Sans Serif.