diff options
| -rw-r--r-- | Utilities/Scripts/update-third-party.bash | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/Utilities/Scripts/update-third-party.bash b/Utilities/Scripts/update-third-party.bash index 3b8358e..670946e 100644 --- a/Utilities/Scripts/update-third-party.bash +++ b/Utilities/Scripts/update-third-party.bash @@ -52,6 +52,14 @@ git_archive () { tar -C "$extractdir" -x } +disable_custom_gitattributes() { + pushd "${extractdir}/${name}-reduced" + # Git does not allow custom attributes in a subdirectory where we + # are about to merge the `.gitattributes` file, so disable them. + sed -i '/^\[attr\]/ {s/^/#/}' .gitattributes + popd +} + die () { echo >&2 "$@" exit 1 |