diff options
| -rwxr-xr-x | invoke_session_debian | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/invoke_session_debian b/invoke_session_debian index 9c6986f..b225c77 100755 --- a/invoke_session_debian +++ b/invoke_session_debian @@ -15,8 +15,16 @@ abe_branch="$2" export benchmark="$3" export toolchain="$4" export targets="$5" -export run_flags="$6" -export compiler_flags="$7" +if test x"$6" = xNone; then + export run_flags= +else + export run_flags="$6" +fi +if test x"$7" = xNone; then + export compiler_flags= +else + export compiler_flags="$7" +fi echo "Target's Gateway: $gateway" env |