From cff434eef64420bbc8b2292670c5417d72b6c7a8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 6 Mar 2018 18:15:38 +0100
Subject: document -profile in dev/doc/setup.txt

---
 dev/doc/setup.txt | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'dev')

diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt
index 0003a2c217..c48c2d5d16 100644
--- a/dev/doc/setup.txt
+++ b/dev/doc/setup.txt
@@ -41,15 +41,15 @@ Building coqtop:
   cd ~/git/coq
   git checkout trunk
   make distclean
-  ./configure -annotate -local
+  ./configure -profile devel
   make clean
   make -j4 coqide printers
 
-The "-annotate" option is essential when one wants to use Merlin.
+The "-profile devel" enables all options recommended for developers (like
+warnings, support for Merlin, etc).  Moreover Coq is configured so that
+it can be run without installing it (i.e. from the current directory).
 
-The "-local" option is useful if one wants to run the coqtop and coqide binaries without running make install
-
-Then check if
+Once the compilation is over check if
 - bin/coqtop
 - bin/coqide
 behave as expected.
-- 
cgit v1.2.3