summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-03-20 13:47:39 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-03-20 13:47:39 -0400
commit758c3e1ffdcaa9aec7b85b6104d6ce03632011ec (patch)
treef760a1894f8588f5e6b33724d3bf7339818358b2 /doc
parentb656abc33d2a0235ebf53097be398b04df17e2b6 (diff)
'--without-emacs' configure option
Diffstat (limited to 'doc')
-rw-r--r--doc/manual.tex2
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index c39d92df..5deb66fc 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -85,6 +85,8 @@ To use the Emacs mode, you must have a modern Emacs installed. We assume that y
apt-get install emacs-goodies-el
\end{verbatim}
+If you don't want to install the Emacs mode, run \texttt{./configure} with the argument \texttt{--without-emacs}.
+
Even with the right packages installed, configuration and building might fail to work. After you run \texttt{./configure}, you will see the values of some named environment variables printed. You may need to adjust these values to get proper installation for your system. To change a value, store your preferred alternative in the corresponding UNIX environment variable, before running \texttt{./configure}. For instance, here is how to change the list of extra arguments that the Ur/Web compiler will pass to GCC on every invocation.
\begin{verbatim}