Deprecate build_tools.sh

2019-07-19 20:54:02 -04:00
parent 20863ac85b
commit 4a239c4604
3 changed files with 20 additions and 10 deletions
@@ -30,7 +30,7 @@ matrix:
            - g++-7
      env: _="Build"
      script:
-        - ./build_tools.sh g++-7
+        - make -j2 tools CXX=g++-7
        - make -j2 compare
        - make -j2 modern
 after_success: