Skip to content

Commit 8650f00

Browse files
Add explanation of "benchmark definition" in glossary
1 parent d38deb9 commit 8650f00

1 file changed

Lines changed: 4 additions & 0 deletions

File tree

doc/INDEX.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,10 @@ BenchExec always uses the SI standard units:
5050

5151
### Glossary
5252

53+
- **benchmark definition**: Input file for `benchexec`
54+
([explanation](benchexec.md#input-for-benchexec), [schema](benchmark.dtd), [documented example](benchmark.xml)),
55+
consists of one or more *run definitions* and one or more sets of *tasks*.
56+
5357
- **executable**: The executable file that is used to start a tool.
5458

5559
- **option**: A command-line argument for a tool.

0 commit comments

Comments
 (0)