diff options
| author | herbelin | 2008-06-01 20:18:52 +0000 |
|---|---|---|
| committer | herbelin | 2008-06-01 20:18:52 +0000 |
| commit | 026930883cfe2e1a431cc0259ed7f2cf2767c201 (patch) | |
| tree | 7b87294e26af25e5ddf433bd830210099ad9da45 | |
| parent | 5e3a747ec4351a6cb07ac307196bad782bca1623 (diff) | |
On cesse de demander une valeur pour l'option reals si l'utilisateur
n'en donne pas (ça paraît plus simple vu que le temps de compil de
reals est devenu mineur, et on fait comme pour fsets qui par défaut
est compilé).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11031 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rwxr-xr-x | configure | 21 |
1 files changed, 2 insertions, 19 deletions
@@ -109,9 +109,7 @@ emacs_spec=no camldir_spec=no lablgtkdir_spec=no coqdocdir_spec=no -fsets_opt=no fsets=all -reals_opt=no reals=all arch_spec=no coqide_spec=no @@ -130,7 +128,6 @@ while : ; do prefix="$2" shift;; -local|--local) local=true - reals_opt=yes reals=all;; -src|--src) src_spec=yes COQSRC="$2" @@ -171,14 +168,12 @@ while : ; do -opt|--opt) bytecamlc=ocamlc.opt camlp4oexec=camlp4o # can't add .opt since dyn load'll be required nativecamlc=ocamlopt.opt;; - -fsets|--fsets) fsets_opt=yes - case "$2" in + -fsets|--fsets) case "$2" in yes|all) fsets=all;; *) fsets=basic esac shift;; - -reals|--reals) reals_opt=yes - case "$2" in + -reals|--reals) case "$2" in yes|all) reals=all;; *) reals=basic esac @@ -713,18 +708,6 @@ case $coqdocdir_spec/$prefix_spec/$local in esac;; esac -case $reals_opt in - no) echo "Should I compile the complete theory of real analysis [Y/N, default is Y] ?" - read reals_ans - - case $reals_ans in - "N"|"n"|"No"|"NO"|"no") - reals=basic;; - *) reals=all;; - esac;; - yes) true;; -esac - # case $emacs_spec in # no) echo "Which Emacs command should I use to compile coq.el [$emacs_def] ?" # read EMACS |