# HG changeset patch
# User John W. Eaton <jwe@octave.org>
# Date 1368725557 14400
# Node ID eb1643bd900c5c1ad8f818ab03d5f7f9d3e5f07f
# Parent  d198aea15b35532af9d674c3ba8a6c6211550afa
mk-dist: new argument, --no-strip

diff -r d198aea15b35 -r eb1643bd900c mk-dist
--- a/mk-dist	Tue May 14 19:26:43 2013 -0400
+++ b/mk-dist	Thu May 16 13:32:37 2013 -0400
@@ -5,6 +5,8 @@
 jobs=9
 
 OCTAVE_TARGET=octave
+
+strip=yes
 while [ $# -gt 0 ]; do
   case "$1" in
     --jobs)
@@ -21,6 +23,10 @@
       OCTAVE_TARGET=stable-octave
       shift
     ;;
+    --no-strip)
+      strip=no
+      shift
+    ;;
     *)
       echo "mk-dist: unrecognized option: $1" 1>&2
       exit 1
@@ -86,12 +92,14 @@
 echo "making all files writable by user..."
 chmod -R u+w $OCTAVE_DIST_DIR
 
-echo "stripping files..."
-cd $OCTAVE_DIST_DIR
-for f in $(find . -name '*.dll' -o -name '*.exe'); do
-  echo "  $f"
-  $STRIP $f
-done
+if [ $strip = "yes" ]; then
+  echo "stripping files..."
+  cd $OCTAVE_DIST_DIR
+  for f in $(find . -name '*.dll' -o -name '*.exe'); do
+    echo "  $f"
+    $STRIP $f
+  done
+fi
 
 #echo "creating tar file..."
 #cd $TOPDIR/dist