2015-11-18 10:00:56 +01:00
|
|
|
# This provides the extglob function to expand wildcards in the destdir
|
|
|
|
|
|
|
|
expand_destdir() {
|
2015-11-18 11:19:09 +01:00
|
|
|
local result= glob= file=
|
2015-11-18 10:00:56 +01:00
|
|
|
|
2015-11-18 11:19:09 +01:00
|
|
|
(
|
|
|
|
set -f
|
|
|
|
for glob in $@; do
|
|
|
|
files=$(echo "${PKGDESTDIR}/${glob}")
|
|
|
|
set +f
|
|
|
|
for file in $files; do
|
|
|
|
result+="${blank}${file#$PKGDESTDIR/}"
|
|
|
|
blank=" "
|
|
|
|
done
|
|
|
|
done
|
|
|
|
echo "$result"
|
|
|
|
)
|
2015-11-18 10:00:56 +01:00
|
|
|
}
|