circleci: rename "-Dbuild_docs" -> "-Dwith_docs"

This was renamed in commit 3f2a671, but I think it was simply forgotten
in CI.
This commit is contained in:
Thiago Kenji Okada 2021-01-06 00:08:21 -03:00
parent d974367a04
commit acadafb073
1 changed files with 1 additions and 1 deletions

View File

@ -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: