diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-07-11 18:46:50 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-07-11 18:46:50 +0200 |
| commit | 143e0aed0a517335160c11d88ffcc26ef4297445 (patch) | |
| tree | bd6e58cef6bfc74c6bc22e4b1f41278a7ab71b97 /tools | |
| parent | 0e09dc477c131a404f28be373effc3508c99ff6f (diff) | |
| download | ocaml-143e0aed0a517335160c11d88ffcc26ef4297445.tar.gz | |
Revert "Temporary: collect timings for tests during the Jenkins CI"
Enough timings were collected for now.
This reverts commit c53a485042dce98a86e15151bb9ab6b21677e956.
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/ci/inria/main | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tools/ci/inria/main b/tools/ci/inria/main index 602c8b6c36..5bf16731fe 100755 --- a/tools/ci/inria/main +++ b/tools/ci/inria/main @@ -273,9 +273,8 @@ rm -rf "$instdir" cd testsuite if test -n "$jobs" && test -x /usr/bin/parallel -then PARALLEL="$jobs $PARALLEL" \ - $make --warn-undefined-variables SHOW_TIMINGS=1 parallel -else $make --warn-undefined-variables SHOW_TIMINGS=1 all +then PARALLEL="$jobs $PARALLEL" $make --warn-undefined-variables parallel +else $make --warn-undefined-variables all fi if $bootstrap; then |