- configure: do not strip coqtop on Darwin so as to support dynamic loading

- configure: remove useless newline (hoping it is OK for everyone)
- coqc: added option -no-glob in accordance with coqc -usage
- coq_makefile: support for installation of all .cmo and all .cmxs in user-contrib




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11676 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 22 insertions, 28 deletions

diff --git a/configure b/configure
index 9ae4f27977..a64f561481 100755
--- a/configure
+++ b/configure
@@ -289,20 +289,6 @@ case $ARCH in
     *) EXE=""
 esac
 
-# strip command
-
-case $ARCH in
-    win32)
-	# true -> strip : it exists under cygwin !
-	STRIPCOMMAND="strip";; 
-    *)
-    if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ]; then
-	STRIPCOMMAND="true"
-    else
-	STRIPCOMMAND="strip"
-    fi
-esac
-
 # Is the source tree checked out from a recognised
 # version control system ?
 if test -e .svn/entries ; then 
@@ -629,12 +615,16 @@ esac
 #CAMLOSTYPE=`config/giveostype`
 #rm config/giveostype
 
+# strip command
+
 case $ARCH in
     win32)
 	# true -> strip : it exists under cygwin !
 	STRIPCOMMAND="strip";; 
     *)
-    if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ]; then
+    if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ] ||
+       [ "`uname -s`" = "Darwin" -a "$HASNATDYNLINK" = "true" ]
+    then
 	STRIPCOMMAND="true"
     else
 	STRIPCOMMAND="strip"
@@ -700,7 +690,7 @@ case $bindir_spec/$prefix_spec/$local in
     yes/*/*) BINDIR=$bindir ;;
     */yes/*) BINDIR=$prefix/bin ;;
     */*/true) BINDIR=$COQTOP/bin ;;
-    *) echo "Where should I install the Coq binaries [$bindir_def] ?"
+    *) printf "Where should I install the Coq binaries [$bindir_def]? "
         read BINDIR
 	case $BINDIR in
 	    "") BINDIR=$bindir_def;;
@@ -716,7 +706,7 @@ case $libdir_spec/$prefix_spec/$local in
           *)  LIBDIR=$prefix/lib/coq ;;
         esac ;;
     */*/true) LIBDIR=$COQTOP ;;
-    *)  echo "Where should I install the Coq library [$libdir_def] ?"
+    *)  printf "Where should I install the Coq library [$libdir_def]? "
         read LIBDIR
 	case $LIBDIR in
 	    "") LIBDIR=$libdir_def;;
@@ -728,7 +718,7 @@ case $mandir_spec/$prefix_spec/$local in
     yes/*/*) MANDIR=$mandir;;
     */yes/*) MANDIR=$prefix/man ;;
     */*/true) MANDIR=$COQTOP/man ;;
-    *)  echo "Where should I install the Coq man pages [$mandir_def] ?"
+    *)  printf "Where should I install the Coq man pages [$mandir_def]? "
         read MANDIR
 	case $MANDIR in
 	    "") MANDIR=$mandir_def;;
@@ -740,7 +730,7 @@ case $docdir_spec/$prefix_spec/$local in
     yes/*/*) DOCDIR=$docdir;;
     */yes/*) DOCDIR=$prefix/share/doc/coq ;;
     */*/true) DOCDIR=$COQTOP/man ;;
-    *)  echo "Where should I install the Coq documentation [$docdir_def] ?"
+    *)  printf "Where should I install the Coq documentation [$docdir_def]? "
         read DOCDIR
 	case $DOCDIR in
 	    "") DOCDIR=$docdir_def;;
@@ -756,7 +746,7 @@ case $emacslib_spec/$prefix_spec/$local in
           *)  EMACSLIB=$prefix/share/emacs/site-lisp ;;
         esac ;;
     */*/true) EMACSLIB=$COQTOP/tools/emacs ;;
-    *) echo "Where should I install the Coq Emacs mode [$emacslib_def] ?"
+    *) printf "Where should I install the Coq Emacs mode [$emacslib_def]? "
         read EMACSLIB
 	case $EMACSLIB in
 	    "") EMACSLIB=$emacslib_def;;
@@ -772,7 +762,7 @@ case $coqdocdir_spec/$prefix_spec/$local in
           *)  COQDOCDIR=$prefix/share/emacs/site-lisp ;;
         esac ;;
     */*/true) COQDOCDIR=$COQTOP/tools/coqdoc ;;
-    *) echo "Where should I install Coqdoc TeX/LaTeX files [$coqdocdir_def] ?"
+    *) printf "Where should I install Coqdoc TeX/LaTeX files [$coqdocdir_def]? "
         read COQDOCDIR
 	case $COQDOCDIR in
 	    "") COQDOCDIR=$coqdocdir_def;;
@@ -789,7 +779,7 @@ case $coqrunbyteflags_spec/$local in
 esac
 
 # case $emacs_spec in
-#     no) echo "Which Emacs command should I use to compile coq.el [$emacs_def] ?"
+#     no) printf "Which Emacs command should I use to compile coq.el [$emacs_def]? "
 #         read EMACS
 	
 # 	case $EMACS in
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index ca1763ce24..bee9e7b329 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -150,13 +150,13 @@ let parse_args () =
     | "-R" as o :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem
 
     | ("-notactics"|"-debug"|"-nolib"
-      | "-debugVM"|"-alltransp"|"-VMno"
+      |"-debugVM"|"-alltransp"|"-VMno"
       |"-batch"|"-nois" | "-noglob" | "-no-glob"
       |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
       |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
       |"-dont-load-proofs"|"-impredicative-set"|"-vm" 
-      | "-unboxed-values" | "-unboxed-definitions" | "-draw-vm-instr" 
-	  as o) :: rem ->
+      |"-unboxed-values"|"-unboxed-definitions"|"-draw-vm-instr"
+      |"-no-glob"|"-noglob" as o) :: rem ->
 	parse (cfiles,o::args) rem
 
     | "-where" :: _ -> 
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index fa5ded938d..52923ad4e3 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -97,9 +97,13 @@ let standard sds sps =
   if !opt = "" then print "\t@echo \"WARNING: opt is disabled\"\n";
   print "\t$(MAKE) all \"OPT:="; print !opt; print "\"\n\n";
   print "install:\n";
-  print "\tmkdir -p `$(COQC) -where`/user-contrib\n";
-  if !some_vfile then print "\tcp -f $(VOFILES) `$(COQC) -where`/user-contrib\n";
-  if !some_mlfile then print "\tcp -f *.cmo `$(COQC) -where`/user-contrib\n";
+  print "\tmkdir -p $(COQLIB)/user-contrib\n";
+  if !some_vfile then
+    print "\tcp -f $(VOFILES) $(COQLIB)/user-contrib\n";
+  if !some_mlfile then
+    print "\tcp -f $(CMOFILES) $(COQLIB)/user-contrib\n";
+  if Coq_config.has_natdynlink && !some_mlfile then
+    print "\tcp -f $(CMXSFILES) $(COQLIB)/user-contrib\n";
   List.iter
     (fun x -> print "\t(cd "; print x; print " ; $(MAKE) install)\n")
     sds;