diff doc/manual.tex @ 1441:8524a1709821

'--without-emacs' configure option
author Adam Chlipala <adam@chlipala.net>
date Sun, 20 Mar 2011 13:47:39 -0400
parents 3dab4696d116
children bd6b03bc6333
line wrap: on
line diff
--- a/doc/manual.tex	Sun Mar 20 13:15:11 2011 -0400
+++ b/doc/manual.tex	Sun Mar 20 13:47:39 2011 -0400
@@ -85,6 +85,8 @@
 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}