diff options
| author | Jason Gross | 2017-05-23 18:30:22 -0400 |
|---|---|---|
| committer | GitHub | 2017-05-23 18:30:22 -0400 |
| commit | 004b82086b1c546e962abeac2fe91d600a304813 (patch) | |
| tree | 09981bcf9ab61bf1733c6619854758577d9724a8 /dev | |
| parent | a2d43679596d86033ac52c16ac137d8cf2a06412 (diff) | |
Add parsers-examples target to fiat-parsers ci
This tests a bit more of fiat-parsers, adding an extra ~3 minutes to the build.
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/ci/ci-fiat-parsers.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh index c62aa1d859..d8460bc70c 100755 --- a/dev/ci/ci-fiat-parsers.sh +++ b/dev/ci/ci-fiat-parsers.sh @@ -7,4 +7,4 @@ fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR} -( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers ) +( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers parsers-examples ) |