diff options
author | Adam Chlipala <adam@chlipala.net> | 2011-08-07 13:47:15 -0400 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2011-08-07 13:47:15 -0400 |
commit | 4e0410306a4d4288dd36450dc8f9ea2e8bd0a154 (patch) | |
tree | b25817bdd61bef40649cdd12b33d6238c67d1fd5 /doc | |
parent | f8d463b31a6808a1b83fa5873f295006b73daf72 (diff) |
Manual: emphasize how great '-tc' is
Diffstat (limited to 'doc')
-rw-r--r-- | doc/manual.tex | 1 |
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} |