diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-07-06 08:59:56 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-07-06 08:59:56 +0200 |
| commit | c53a485042dce98a86e15151bb9ab6b21677e956 (patch) | |
| tree | 7c9d404db6b88c7c809c2f0aaef2878236fc3e67 /tools | |
| parent | cefde00c6f6e81ae485a5fc924b8a45e5d8d3f8a (diff) | |
| download | ocaml-c53a485042dce98a86e15151bb9ab6b21677e956.tar.gz | |
Temporary: collect timings for tests during the Jenkins CI
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/ci/inria/main | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tools/ci/inria/main b/tools/ci/inria/main index 2244e4c66d..871282f5d9 100755 --- a/tools/ci/inria/main +++ b/tools/ci/inria/main @@ -273,8 +273,9 @@ rm -rf "$instdir" cd testsuite if test -n "$jobs" && test -x /usr/bin/parallel -then PARALLEL="$jobs $PARALLEL" $make --warn-undefined-variables parallel -else $make --warn-undefined-variables all +then PARALLEL="$jobs $PARALLEL" \ + $make --warn-undefined-variables SHOW_TIMINGS=1 parallel +else $make --warn-undefined-variables SHOW_TIMINGS=1 all fi if $bootstrap; then |