summaryrefslogtreecommitdiff
path: root/tests/README.md
diff options
context:
space:
mode:
Diffstat (limited to 'tests/README.md')
-rw-r--r--tests/README.md2
1 files changed, 1 insertions, 1 deletions
diff --git a/tests/README.md b/tests/README.md
index 4f4f1ff5..f68b509f 100644
--- a/tests/README.md
+++ b/tests/README.md
@@ -50,7 +50,7 @@ In both cases it supports the same options. Typical options are:
- `[fstar] known-failure`: see below;
- `[coq,fstar] subdir=misc`: store the output in the `misc` subdirectory for these two backends.
-For an up-to-date list of options, see comments in the test runner code.
+For an up-to-date list of options, see comments in `tests/test_runner/Input.ml`.
# `known-failure` tests