diff options
| author | Gaëtan Gilbert | 2018-10-15 12:58:45 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-15 12:58:45 +0200 |
| commit | 13ddbed6afa8a1917e3906c8b92f5bf56d3f2377 (patch) | |
| tree | d33a0668e4f8473bbe99e9e08a23702038ecf3b5 | |
| parent | 3a552450ddcdf96ef5b12be19ad67207697d298c (diff) | |
| parent | 043a7f049e3e88e91317524dfc5d9b06c89fdbe7 (diff) | |
Merge PR #8732: [ci] [sf] Remove sed hacks from the SF build.
| -rwxr-xr-x | dev/ci/ci-sf.sh | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 58bbb7229f..60436e672c 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -8,11 +8,6 @@ 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 - -( cd lf && make clean && make ) - -( cd plf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make ) - +( cd lf && make clean && make ) +( cd plf && make clean && make ) ( cd vfa && make clean && make ) |