diff options
| author | Maxime Dénès | 2017-06-14 19:00:23 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-14 19:00:23 +0200 |
| commit | e1d68573015883301cb401861e10233f6442d9ec (patch) | |
| tree | b62f4d6f0f2cfdd09cbe6080f66ec8c92024fbce /dev | |
| parent | 54063fcda793ca8179047ff2a2c9863891a97acd (diff) | |
| parent | 9a14a95f96c77ff3850d694637738358c164f4b5 (diff) | |
Merge PR#749: Normalize deprecation notices of ./configure
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/setup.txt | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt index 1b016a4e26..0c6d3ee80d 100644 --- a/dev/doc/setup.txt +++ b/dev/doc/setup.txt @@ -12,7 +12,7 @@ How to compile Coq Getting build dependencies: - sudo apt-get install make opam git mercurial darcs + sudo apt-get install make opam git opam init --comp 4.02.3 # Then follow the advice displayed at the end as how to update your ~/.bashrc and ~/.ocamlinit files. @@ -41,7 +41,7 @@ Building coqtop: cd ~/git/coq git checkout trunk make distclean - ./configure -annotate -with-doc no -local -debug -usecamlp5 + ./configure -annotate -local make clean make -j4 coqide printers @@ -49,8 +49,6 @@ The "-annotate" option is essential when one wants to use Merlin. The "-local" option is useful if one wants to run the coqtop and coqide binaries without running make install -The "-debug" option is essential if one wants to use ocamldebug with the coqtop binary. - Then check if - bin/coqtop - bin/coqide @@ -60,7 +58,7 @@ behave as expected. A note about rlwrap ------------------- -Running "coqtop" under "rlwrap" is possible, but there is a catch. If you try: +Running "coqtop" under "rlwrap" is possible, but (on Debian) there is a catch. If you try: cd ~/git/coq rlwrap bin/coqtop |