diff options
| author | Emilio Jesus Gallego Arias | 2017-12-09 02:06:41 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-12-09 03:18:11 +0100 |
| commit | 751375678bfee0cf3abb05dafe79fcf5689c4fce (patch) | |
| tree | 8b06feec7de3fcd9bc90ed91c5393e3f433daf95 /dev/ci | |
| parent | 7b40908bfbc255d51384e88a73fa5d98380b237f (diff) | |
[ci] Download ci-sf archives into the proper CI build dir.
Currently, `make ci-sf` downloads and builds the files in the main root
directory. we fix that.
Diffstat (limited to 'dev/ci')
| -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 217540cc19..4e8c7e145e 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 |