diff options
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/appveyor.bat | 14 | ||||
| -rwxr-xr-x | dev/ci/ci-geocoq.sh | 6 |
2 files changed, 11 insertions, 9 deletions
diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat index ca6a5643c1..e2fbf1f6d1 100644 --- a/dev/ci/appveyor.bat +++ b/dev/ci/appveyor.bat @@ -23,13 +23,19 @@ if %USEOPAM% == false ( call %APPVEYOR_BUILD_FOLDER%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^ -arch=%ARCH% -installer=Y -coqver=%APPVEYOR_BUILD_FOLDER_CFMT% ^ -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^ - -setup %CYGROOT%\%SETUP% - copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis - 7z a coq-opensource-archive-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* + -setup %CYGROOT%\%SETUP% || GOTO ErrorExit + copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit + 7z a coq-opensource-archive-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit ) if %USEOPAM% == true ( %CYGROOT%\%SETUP% -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% ^ -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time - %CYGROOT%/bin/bash -l %APPVEYOR_BUILD_FOLDER%/dev/ci/appveyor.sh + %CYGROOT%/bin/bash -l %APPVEYOR_BUILD_FOLDER%/dev/ci/appveyor.sh || GOTO ErrorExit ) + +GOTO :EOF + +:ErrorExit + ECHO ERROR MakeCoq_MinGW.bat failed + EXIT /b 1 diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index eadeb7c38c..8e6448e764 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -8,9 +8,5 @@ GeoCoq_CI_DIR=${CI_BUILD_DIR}/GeoCoq git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR} ( cd ${GeoCoq_CI_DIR} && \ - ./configure.sh && \ - sed -i.bak '/Ch16_coordinates_with_functions\.v/d' Make && \ - sed -i.bak '/Elements\/Book_1\.v/d' Make && \ - sed -i.bak '/Elements\/Book_3\.v/d' Make && \ - coq_makefile -f Make -o Makefile && \ + ./configure-ci.sh && \ make ) |