diff options
Diffstat (limited to 'tests/README.md')
-rw-r--r-- | tests/README.md | 2 |
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 |