From 2b27d436e36f7ae2173797fb22fa24a2b058dc13 Mon Sep 17 00:00:00 2001
From: Hans-Peter Deifel <hpd@hpdeifel.de>
Date: Wed, 21 Feb 2018 16:53:36 +0100
Subject: [PATCH] Document requirement of `perf` better

---
 README.txt                   | 9 +++++++++
 scripts/bench_one_formula.sh | 4 ++++
 2 files changed, 13 insertions(+)

diff --git a/README.txt b/README.txt
index 39ed1d1..ffdff44 100644
--- a/README.txt
+++ b/README.txt
@@ -75,6 +75,15 @@ following columns:
 
   - states: Number of states in the resulting parity game.
 
+## Getting the standard derivation
+
+This requires the additional tool `perf`. Install it with:
+
+    apt install linux-tools-common
+
+and change the variable TIME_COMMAND in `bench_one_formula.sh` as
+documented there.
+
 ## More information
 
 The various scripts in `scripts` contain comments that explain how to
diff --git a/scripts/bench_one_formula.sh b/scripts/bench_one_formula.sh
index bf5b725..2662ff7 100755
--- a/scripts/bench_one_formula.sh
+++ b/scripts/bench_one_formula.sh
@@ -21,6 +21,10 @@
 # measurements and must output "X seconds time elapsed" for collect_output.pl to
 # be able to parse it.
 #
+# `/usr/bin/time` doesn't run the program multiple times and computes no
+# standard derivation. For this you'd have to install the Linux tool `perf` and
+# set TIME_COMMAND as in the first example.
+#
 # Examples:
 #   - perf stat -rNUM   # NUM is the repeat count
 #   - /usr/bin/time --format "%e seconds time elapsed"
-- 
GitLab