Retrait du 'strip' en cas de profiling

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

2 files changed, 8 insertions, 3 deletions

diff --git a/config/Makefile.template b/config/Makefile.template
index 52c054372b..07e9089c85 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -104,9 +104,10 @@ INSTALL=COQTOPDIRECTORY/bin/ARCHITECTURE/coqinstallEXECUTEEXTENSION
 MKDIR=mkdir -p
 
 #the command STRIP 
-# Unix systems: strip
+# Unix systems and profiling: true
+# Unix systems and no profiling: strip
 # Win32 systems: true (actually strip is bogus)
 STRIP=STRIPCOMMAND
 
 # make or sed are bogus and believe lines not terminating by a return
-# are inexistent
\ No newline at end of file
+# are inexistent
diff --git a/configure b/configure
index 46c49daa87..3c890cf90d 100755
--- a/configure
+++ b/configure
@@ -342,7 +342,11 @@ case $ARCH in
     win32)
 	STRIPCOMMAND="true";;
     *)
-	STRIPCOMMAND="strip";;
+    if test $coq_profile_flag = "-p" ; then
+	STRIPCOMMAND="true"
+    else
+	STRIPCOMMAND="strip"
+    fi
 esac
 
 # Summary of the configuration