diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 14:18:30 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 14:18:30 +0100 |
commit | e9d2a40ed12e31095565b5c7401f02af997a7cc7 (patch) | |
tree | 72ddf992c1f2eb68cafd7bcf2acac6cc5b13e47b /dev | |
parent | 88ac5d92ce1a2f97c805f715021b2fed3f4c624f (diff) | |
parent | cff434eef64420bbc8b2292670c5417d72b6c7a8 (diff) |
Merge PR #6817: [configure]: support for profiles
Diffstat (limited to 'dev')
-rw-r--r-- | dev/doc/setup.txt | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt index 0003a2c21..c48c2d5d1 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. |