diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-11 09:31:12 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-11 09:31:12 +0100 |
| commit | f936f89361145bea242ae6461ba2d6f90f4554cd (patch) | |
| tree | d4ec39c0474681cbd802ec73e2e76476ce1b1d7a /dev | |
| parent | b1b84b3a942375048db459d81d2b9bc7662f6ada (diff) | |
| parent | 751375678bfee0cf3abb05dafe79fcf5689c4fce (diff) | |
Merge PR #6358: [ci] Download ci-sf archives into the proper CI build dir.
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/ci/ci-sf.sh | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 217540cc1..4e8c7e145 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -3,13 +3,10 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -# XXX: Needs fixing to properly set the build directory. -wget ${sf_lf_CI_TARURL} -wget ${sf_plf_CI_TARURL} -wget ${sf_vfa_CI_TARURL} -tar xvfz lf.tgz -tar xvfz plf.tgz -tar xvfz vfa.tgz +mkdir -p ${CI_BUILD_DIR} && cd ${CI_BUILD_DIR} +wget -qO- ${sf_lf_CI_TARURL} | tar xvz +wget -qO- ${sf_plf_CI_TARURL} | tar xvz +wget -qO- ${sf_vfa_CI_TARURL} | tar xvz sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v |