Allow pushFilter regex to start with a dash

This commit is contained in:
Claudio Bley 2021-08-04 09:09:00 +02:00 committed by GitHub
commit fccf77d171
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -4,7 +4,7 @@ set -euo pipefail
PATHS=$(comm -13 <(sort /tmp/store-path-pre-build) <("$(dirname "$0")"/list-nix-store.sh)) PATHS=$(comm -13 <(sort /tmp/store-path-pre-build) <("$(dirname "$0")"/list-nix-store.sh))
if [[ $3 != "" ]]; then if [[ $3 != "" ]]; then
PATHS=$(echo "$PATHS" | grep -vE "$3") PATHS=$(echo "$PATHS" | grep -vEe "$3")
fi fi
echo "$PATHS" | "$1" push -j8 "$2" echo "$PATHS" | "$1" push -j8 "$2"