diff options
| author | Maxime Dénès | 2017-05-26 00:29:53 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-26 00:29:53 +0200 |
| commit | fa400ee741c2d32427e39bd860edfcd27dc719d3 (patch) | |
| tree | dbed634a8a7e340d80dbf69d1e2de67cf7663be4 | |
| parent | 90fa7d931f45673df93d57f77e74af51a180db9d (diff) | |
| parent | 004b82086b1c546e962abeac2fe91d600a304813 (diff) | |
Merge PR#672: Add parsers-examples target to fiat-parsers ci
| -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 ) |