Merge remote-tracking branch 'origin/dev' into dev

This commit is contained in:
Johannes Theiner 2020-01-08 19:13:01 +01:00
commit ced2aca75f

View File

@ -31,7 +31,7 @@ make_test:
- docker-ci - docker-ci
script: script:
- apt-get update - apt-get update
- apt-get install -y g++ make cmake clang-tidy - apt-get install -y clang make cmake clang-tidy
- mkdir current - mkdir current
- ls | grep -v current | xargs mv -t current - ls | grep -v current | xargs mv -t current
- git clone https://github.com/catchorg/Catch2.git - git clone https://github.com/catchorg/Catch2.git
@ -57,7 +57,7 @@ cmake_build:
- docker-ci - docker-ci
script: script:
- apt-get update - apt-get update
- apt-get install -y g++ make cmake clang-tidy - apt-get install -y clang make cmake clang-tidy
- mkdir current - mkdir current
- ls | grep -v current | xargs mv -t current - ls | grep -v current | xargs mv -t current
- git clone https://github.com/catchorg/Catch2.git - git clone https://github.com/catchorg/Catch2.git