diff --git a/download.html b/download.html
index d594d7c723a4dcaaa1590f002bba114bc1220616_ZG93bmxvYWQuaHRtbA==..931d37691287e5a69c62e989f8252b80f319cb17_ZG93bmxvYWQuaHRtbA== 100644
--- a/download.html
+++ b/download.html
@@ -155,6 +155,7 @@
 JIT is delicate.  It requires using either MSVC or gcc with no particularly
 fancy options.  It does not work e.g. with clang, or if you pass uncommon
 options with the <tt class="docutils literal">CFLAGS</tt> environment variable.  The generated C files
-are left around in <tt class="docutils literal"><span class="pre">/tmp/usession-$USER/testing_1/</span></tt>, so if compilation
+are left around in <tt class="docutils literal"><span class="pre">/tmp/usession-$USER/testing_1/</span></tt> or
+<tt class="docutils literal"><span class="pre">$TMPDIR/usession-$USER/testing_1</span></tt>, so if compilation
 fails (i.e. you get a <tt class="docutils literal">CompilationError</tt>) or if you want to build a
 debug build, you can go there and retry running <tt class="docutils literal">make</tt>.  For example:
@@ -159,7 +160,7 @@
 fails (i.e. you get a <tt class="docutils literal">CompilationError</tt>) or if you want to build a
 debug build, you can go there and retry running <tt class="docutils literal">make</tt>.  For example:
-<tt class="docutils literal">make <span class="pre">CFLAGS=&quot;&quot;</span></tt>, or <tt class="docutils literal">make lldebug</tt>.  It is recommended to move this
-directory away if you want to keep it; otherwise, further runs of
+<tt class="docutils literal">CFLAGS= make</tt>, or <tt class="docutils literal">make lldebug</tt>.  It is recommended to move this
+directory away if you want to keep it; otherwise, future runs of
 <tt class="docutils literal">translate.py</tt> will remove it.</li>
 </ul>
 </div>
diff --git a/source/download.txt b/source/download.txt
index d594d7c723a4dcaaa1590f002bba114bc1220616_c291cmNlL2Rvd25sb2FkLnR4dA==..931d37691287e5a69c62e989f8252b80f319cb17_c291cmNlL2Rvd25sb2FkLnR4dA== 100644
--- a/source/download.txt
+++ b/source/download.txt
@@ -142,6 +142,7 @@
   JIT is delicate.  It requires using either MSVC or gcc with no particularly
   fancy options.  It does not work e.g. with clang, or if you pass uncommon
   options with the ``CFLAGS`` environment variable.  The generated C files
-  are left around in ``/tmp/usession-$USER/testing_1/``, so if compilation
+  are left around in ``/tmp/usession-$USER/testing_1/`` or
+  ``$TMPDIR/usession-$USER/testing_1``, so if compilation
   fails (i.e. you get a ``CompilationError``) or if you want to build a
   debug build, you can go there and retry running ``make``.  For example:
@@ -146,7 +147,7 @@
   fails (i.e. you get a ``CompilationError``) or if you want to build a
   debug build, you can go there and retry running ``make``.  For example:
-  ``make CFLAGS=""``, or ``make lldebug``.  It is recommended to move this
-  directory away if you want to keep it; otherwise, further runs of
+  ``CFLAGS= make``, or ``make lldebug``.  It is recommended to move this
+  directory away if you want to keep it; otherwise, future runs of
   ``translate.py`` will remove it.
 
 .. _`x86 (IA-32)`: http://en.wikipedia.org/wiki/IA-32