diff options
author | 2017-06-08 11:17:22 +0200 | |
---|---|---|
committer | 2017-06-11 10:26:07 +0200 | |
commit | 9a14a95f96c77ff3850d694637738358c164f4b5 (patch) | |
tree | 8d1ba78033d0e209fbaba7ba7ace7980a67b0c41 /dev/doc | |
parent | 102d7418e399de646b069924277e4baea1badaca (diff) |
Normalize deprecation notices of ./configure
Always output a warning on stderr when a deprecated option is used.
Diffstat (limited to 'dev/doc')
-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 1b016a4e2..0c6d3ee80 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 |