]> https://gitweb.dealii.org/ - dealii.git/commit
projects / dealii.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e9beea2) | patch
Indent script: Do not use --diff-filter=d 9511/head
authorMatthias Maier <tamiko@43-1.org>
Tue, 11 Feb 2020 17:15:44 +0000 (11:15 -0600)
committerMatthias Maier <tamiko@43-1.org>
Tue, 11 Feb 2020 17:15:44 +0000 (11:15 -0600)
commitac0f23f2826e9ff1fc8afa18fde5297bc95f6d25
tree986e5efaf50bdbf360987fb0bf9fe44d11b15549tree | snapshot
parente9beea244a184dbf2ffc4661f7903f6cfd8f3916commit | diff
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
contrib/utilities/indent_common.sh diff | blob | history
Mirror of the development repository for deal.II

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.