diff options
| -rwxr-xr-x | devscripts/release.sh | 6 | 
1 files changed, 3 insertions, 3 deletions
diff --git a/devscripts/release.sh b/devscripts/release.sh index 323acf8cf..72e708c7f 100755 --- a/devscripts/release.sh +++ b/devscripts/release.sh @@ -14,9 +14,9 @@  set -e -skip_tests=false -if [ "$1" = '--skip-test' ]; then -    skip_tests=true +skip_tests=true +if [ "$1" = '--run-tests' ]; then +    skip_tests=false      shift  fi  | 
