From acadafb0735a7364a13090760c610a7039fd0f41 Mon Sep 17 00:00:00 2001 From: Thiago Kenji Okada Date: Wed, 6 Jan 2021 00:08:21 -0300 Subject: [PATCH] circleci: rename "-Dbuild_docs" -> "-Dwith_docs" This was renamed in commit 3f2a671, but I think it was simply forgotten in CI. --- .circleci/config.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.circleci/config.yml b/.circleci/config.yml index 973a904d..6c348faf 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -39,7 +39,7 @@ jobs: executor: e steps: - build: - build-config: -Dbuild_docs=true -Db_coverage=true + build-config: -Dwith_docs=true -Db_coverage=true - persist_to_workspace: root: . paths: