1 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/run.sh
new file mode 100755
index 0000000000..980bf9cf01
--- /dev/null
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/run.sh
@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+
+set -x
+set -e
+
+cd "$(dirname "${BASH_SOURCE[0]}")"
+
+"$COQLIB"/tools/make-both-single-timing-files.py --fuzz=20 foo.v.after-timing.in foo.v.before-timing.in foo-real.v.timing.diff || exit $?
+
+diff -u foo-real.v.timing.diff.expected foo-real.v.timing.diff || exit $?
+
+"$COQLIB"/tools/make-both-single-timing-files.py --fuzz=20 --user foo.v.after-timing.in foo.v.before-timing.in foo-user.v.timing.diff || exit $?
+
+diff -u foo-user.v.timing.diff.expected foo-user.v.timing.diff || exit $?