diff options
Diffstat (limited to '.github/configs')
-rwxr-xr-x | .github/configs | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/.github/configs b/.github/configs index fdc0b601..404ee7e8 100755 --- a/.github/configs +++ b/.github/configs @@ -55,6 +55,9 @@ case "$config" in LIBCRYPTOFLAGS="--without-openssl" TEST_TARGET=t-exec ;; + valgrind) + TEST_TARGET=USE_VALGRIND=1 + ;; *) echo "Unknown configuration $config" exit 1 |