summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-08-07 13:47:15 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-08-07 13:47:15 -0400
commitc1ff87c8dc39e9c5b550ef6969c0c16b7888f8e6 (patch)
treeb25817bdd61bef40649cdd12b33d6238c67d1fd5 /doc
parent7187b4e8d04500c6648ea49b0f95df567385fce4 (diff)
Manual: emphasize how great '-tc' is
Diffstat (limited to 'doc')
-rw-r--r--doc/manual.tex1
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index 53e1eb8c..a139310c 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -197,6 +197,7 @@ To stop the compilation process after type-checking, run
\begin{verbatim}
urweb -tc P
\end{verbatim}
+It is often worthwhile to run \cd{urweb} in this mode, because later phases of compilation can take significantly longer than type-checking alone, and the type checker catches many errors that would traditionally be found through debugging a running application.
To output information relevant to CSS stylesheets (and not finish regular compilation), run
\begin{verbatim}