From 7813fd122395e0bddf655e6cc87617333e480d23 Mon Sep 17 00:00:00 2001 From: Shahram Najm Date: Sun, 16 Apr 2023 14:11:05 +0100 Subject: [PATCH] EXTRA_TOOLS: retry enabling --- .github/.cmake-options | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.github/.cmake-options b/.github/.cmake-options index ffc099d3c..05fc1f6c2 100644 --- a/.github/.cmake-options +++ b/.github/.cmake-options @@ -1,2 +1 @@ --DENABLE_EXTRA_TESTS=1 --DECCODES_INSTALL_EXTRA_TOOLS=1 +-DENABLE_EXTRA_TESTS=1 -DECCODES_INSTALL_EXTRA_TOOLS=1