# HG changeset patch # User Adam Chlipala # Date 1312739235 14400 # Node ID 09c56e03beafc104c5bb93565fca731d9e72599f # Parent a8a538800278241acd95d4a4f06a985589141ce1 Manual: emphasize how great '-tc' is diff -r a8a538800278 -r 09c56e03beaf doc/manual.tex --- a/doc/manual.tex Sat Aug 06 13:07:50 2011 -0400 +++ b/doc/manual.tex Sun Aug 07 13:47:15 2011 -0400 @@ -197,6 +197,7 @@ \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}