diff options
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/appveyor.bat | 14 | ||||
| -rw-r--r-- | dev/ci/ci-basic-overlay.sh | 4 | ||||
| -rw-r--r-- | dev/ci/ci-common.sh | 1 | ||||
| -rwxr-xr-x | dev/ci/ci-geocoq.sh | 6 |
4 files changed, 14 insertions, 11 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-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 8e7265969b..43525dcd40 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -127,5 +127,5 @@ ######################################################################## # Bignums ######################################################################## -: ${bignums_CI_BRANCH:=fix-thunk-printer} -: ${bignums_CI_GITURL:=https://github.com/ppedrot/bignums.git} +: ${bignums_CI_BRANCH:=master} +: ${bignums_CI_GITURL:=https://github.com/coq/bignums.git} diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 358f527f9e..1bfdf7dfbe 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -5,6 +5,7 @@ set -xe if [ -n "${GITLAB_CI}" ]; then export COQBIN=`pwd`/_install_ci/bin + export TRAVIS_BRANCH="$CI_COMMIT_REF_NAME" else export COQBIN=`pwd`/bin fi 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 ) |