1 files changed, 2 insertions, 2 deletions
diff --git a/configure b/configure
index 1771756c85..07bea069a7 100755
--- a/configure
+++ b/configure
@@ -271,7 +271,7 @@ case $ARCH in
 	# true -> strip : it exists under cygwin !
 	STRIPCOMMAND="strip";; 
     *)
-    if [ "$coq_profile_flag" = "-p" ] ; then
+    if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ]; then
 	STRIPCOMMAND="true"
     else
 	STRIPCOMMAND="strip"
@@ -579,7 +579,7 @@ case $ARCH in
 	# true -> strip : it exists under cygwin !
 	STRIPCOMMAND="strip";; 
     *)
-    if [ "$coq_profile_flag" = "-p" ] ; then
+    if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ]; then
 	STRIPCOMMAND="true"
     else
 	STRIPCOMMAND="strip"