Automatic merge branch 'main' into 'devel'

This commit is contained in:
github-actions[bot] 2023-03-29 08:21:19 +00:00 committed by GitHub
commit 13f005fdb5
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 12 additions and 0 deletions

View File

@ -14,6 +14,10 @@ CCACHE=""
for i in "$@"
do
case $i in
-s=*|--source_path=*)
SOURCE_PATH="${i#*=}"
shift # past argument=value
;;
-b=*|--build_path=*)
BUILD_PATH="${i#*=}"
shift # past argument=value

View File

@ -14,6 +14,10 @@ CCACHE=""
for i in "$@"
do
case $i in
-s=*|--source_path=*)
SOURCE_PATH="${i#*=}"
shift # past argument=value
;;
-b=*|--build_path=*)
BUILD_PATH="${i#*=}"
shift # past argument=value

View File

@ -14,6 +14,10 @@ CCACHE=""
for i in "$@"
do
case $i in
-s=*|--source_path=*)
SOURCE_PATH="${i#*=}"
shift # past argument=value
;;
-b=*|--build_path=*)
BUILD_PATH="${i#*=}"
shift # past argument=value