summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-12-24 10:02:48 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-12-24 10:02:48 -0500
commit07d56b08d87a7453fcd5b192532fcceac86c27cc (patch)
treedc52de3d21f2f622545e1a955a42aff636665da2 /doc
parent53c60e510b1f818cdb0ef7f5456c35e67a431f25 (diff)
-tc flag
Diffstat (limited to 'doc')
-rw-r--r--doc/manual.tex5
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index 11d1b2d9..25c5d9b6 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -168,6 +168,11 @@ To time how long the different compiler phases run, without generating an execut
urweb -timing P
\end{verbatim}
+To stop the compilation process after type-checking, run
+\begin{verbatim}
+urweb -tc P
+\end{verbatim}
+
Some other command-line parameters are accepted:
\begin{itemize}
\item \texttt{-db <DBSTRING>}: Set database connection information, using the format expected by Postgres's \texttt{PQconnectdb()}, which is \texttt{name1=value1 ... nameN=valueN}. The same format is also parsed and used to discover connection parameters for MySQL and SQLite. The only significant settings for MySQL are \texttt{host}, \texttt{hostaddr}, \texttt{port}, \texttt{dbname}, \texttt{user}, and \texttt{password}. The only significant setting for SQLite is \texttt{dbname}, which is interpreted as the filesystem path to the database. Additionally, when using SQLite, a database string may be just a file path.