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

1 files changed, 5 insertions, 1 deletions

diff --git a/configure b/configure
index 46c49daa8..3c890cf90 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