diff options
Diffstat (limited to 'Test/README.md')
| -rw-r--r-- | Test/README.md | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/Test/README.md b/Test/README.md index 4446aa4f..136881a5 100644 --- a/Test/README.md +++ b/Test/README.md @@ -108,22 +108,28 @@ considered to fail. The RUN lines may use several substitutions
- ``%boogie`` expands to the absolute path to the Boogie executable with any set
- options and prefixed by ``mono`` on non Windows platforms
+ options and prefixed by ``mono`` on non Windows platforms. This does not need
+ to be quoted.
- ``%diff`` expands to the diff tool being used. This is ``diff`` on non
Windows platforms and ``pydiff`` on Windows. Do not use the ``fc`` tool
- because it is buggy when tests are run concurrently.
+ because it is buggy when tests are run concurrently. This does not need to be
+ quoted.
-- ``%OutputCheck`` expands to the absolute path to the OutputCheck tool
+- ``%OutputCheck`` expands to the absolute path to the OutputCheck tool. This
+ does not need to be quoted.
-- ``%s`` the absolute path to the current test file
+- ``%s`` the absolute path to the current test file. You should make sure this
+ is quoted so that tests work correctly for users who use spaces in their file
+ paths.
-- ``%T`` the path to the temporary directory for this test
+- ``%T`` the path to the temporary directory for this test. You should make sure
+ this is quoted.
- ``%t`` expands to the absolute path of a filename that can be used as a
temporary file. This always expands to the same value in a single test so if
you need multiple different temporary files append a unique value (e.g.
- ``%t1``, ``%t2``... etc).
+ ``%t1``, ``%t2``... etc). You should make sure this is quoted.
Currently most tests simply execute boogie recording its output which then
compared to a file containing the expected output (``.expect`` files) using
|