Fix lit test suite when running Boogie under a path that contains

spaces.

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