diff options
| -rwxr-xr-x | bin/update_pch.sh | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/bin/update_pch.sh b/bin/update_pch.sh index 61f0c6d74e25..9f423d643d00 100755 --- a/bin/update_pch.sh +++ b/bin/update_pch.sh @@ -8,6 +8,7 @@ # # Usage: update_pch.sh [precompiled_xxx.hxx] +# Invoke: make cmd cmd="./bin/update_pch.sh [..]" root=`dirname $0` root=`cd $root/.. && pwd` @@ -18,6 +19,17 @@ else headers="$1" fi +# Split the headers into an array. +IFS=' ' read -a aheaders <<< $headers +hlen=${#aheaders[@]}; +if [ $hlen -gt 1 ]; then + if [ -z "$PARALLELISM" ]; then + PARALLELISM=0 # Let xargs decide + fi + echo $headers | xargs -n 1 -P $PARALLELISM $0 + exit $? +fi + for x in $headers; do header=$x echo updating `echo $header | sed -e s%$root/%%` |