diff options
Diffstat (limited to 'dev/ci/ci-unimath.sh')
| -rwxr-xr-x | dev/ci/ci-unimath.sh | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh index 62a949f59..aa20fe1ff 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -7,7 +7,4 @@ UniMath_CI_DIR="${CI_BUILD_DIR}/UniMath" git_checkout "${UniMath_CI_BRANCH}" "${UniMath_CI_GITURL}" "${UniMath_CI_DIR}" -( cd "${UniMath_CI_DIR}" && \ - sed -i.bak '/Folds/d' Makefile && \ - sed -i.bak '/HomologicalAlgebra/d' Makefile && \ - make BUILD_COQ=no ) +( cd "${UniMath_CI_DIR}" && make BUILD_COQ=no ) |