From a55c3a12307786375d06b92e0148a7a1c006a971 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Sat, 16 Jun 2018 23:28:47 +0200 Subject: [PATCH] circle: don't mess with pushd I've no idea what pushd is, so stop pretending. --- .circleci/config.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.circleci/config.yml b/.circleci/config.yml index 1026943e14..b241f7f3b6 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -18,6 +18,6 @@ jobs: - run: name: Configure, build and test da stuff command: | - mkdir _build - pushd _build; cmake -Denable_documentation=OFF -Denable_coverage=ON -Denable_java=ON -Denable_model-checking=OFF -Denable_lua=OFF -Denable_compile_optimizations=ON -Denable_smpi=ON -Denable_smpi_MPICH3_testsuite=OFF -Denable_compile_warnings=ON .. - pushd _build ; make -j4 && ctest -j4 --output-on-failure + mkdir _build && cd _build + cmake -Denable_documentation=OFF -Denable_coverage=ON -Denable_java=ON -Denable_model-checking=OFF -Denable_lua=OFF -Denable_compile_optimizations=ON -Denable_smpi=ON -Denable_smpi_MPICH3_testsuite=OFF -Denable_compile_warnings=ON .. + make -j4 && ctest -j4 --output-on-failure -- 2.20.1