diff --git a/doc/scripts/coverage.sh b/doc/scripts/coverage.sh index e8befde..349c122 100755 --- a/doc/scripts/coverage.sh +++ b/doc/scripts/coverage.sh @@ -96,11 +96,14 @@ _usage() #main clean=0 -while getopts "cP:" name; do +while getopts "cO:P:" name; do case "$name" in c) clean=1 ;; + O) + export "${OPTARG%%=*}"="${OPTARG#*=}" + ;; P) #XXX ignored ;;