Commit 9e036a17 authored by Ralf Jung's avatar Ralf Jung
Browse files

TIMING_CONF no longer needs to be set

parent 1c2ae888
......@@ -128,17 +128,15 @@ build-coq.8.10.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.10.0"
TIMING_CONF: "coq-8.10.0"
tags:
- fp-timing
```
The last two lines makes this job run on the more isolated runner. The
`TIMING_CONF` variable triggers measuring the performance of building every
single file of this project. This information is submitted to the [coq-speed]
server where you can browse it in a web UI. Be careful to pick a unique
`TIMING_CONF` if you are timing in multiple jobs, or the build will fail because
of duplicate timing data.
The last two lines makes this job run on the more isolated runner. This
automatically triggers measuring the performance of building every single file
of this project. This information is submitted to the [coq-speed] server where
you can browse it in a web UI. The "configuration" is set to the job name
(i.e., `build-coq.8.10.0` in the example above).
This requires setting the `TIMING_SECRET` CI variable. Talk to an admin about
this. The variable should *not* be protected because we do timing measurements
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment