diff options
| -rwxr-xr-x | utils/NewNightlyTest.pl | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/utils/NewNightlyTest.pl b/utils/NewNightlyTest.pl index 09e6e30c6b..fd38a05cf0 100755 --- a/utils/NewNightlyTest.pl +++ b/utils/NewNightlyTest.pl @@ -181,6 +181,8 @@ while (scalar(@ARGV) and ($_ = $ARGV[0], /^[-+]/)) { shift; next; } if (/^-with-externals$/) { $CONFIGUREARGS .= " --with-externals=$ARGV[0]"; shift; next; } + if (/^-configure-args$/) { $CONFIGUREARGS .= " $ARGV[0]"; + shift; next; } if (/^-submit-server/) { $SUBMITSERVER = "$ARGV[0]"; shift; next; } if (/^-submit-script/) { $SUBMITSCRIPT = "$ARGV[0]"; shift; next; } if (/^-submit-aux/) { $SUBMITAUX = "$ARGV[0]"; shift; next; } |