# HG changeset patch
# User Rik <address@hidden>
# Date 1384296254 28800
#      Tue Nov 12 14:44:14 2013 -0800
# Node ID d36a7702d9b722b77c63d4be993e0feb7dc55683
# Parent  d3cd9b4ccf026a6b89c8f01c1c00526bea5a62cb
mk-dist: Don't use $SHELL in case it is anything other than bash.

* mk-dist: Don't call $SHELL ../makeinst-script.sh.  Just call script
and let #! mechanism sort out the correct shell.

diff -r d3cd9b4ccf02 -r d36a7702d9b7 mk-dist
--- a/mk-dist	Tue Nov 12 14:40:58 2013 -0800
+++ b/mk-dist	Tue Nov 12 14:44:14 2013 -0800
@@ -124,7 +124,7 @@
 cd $TOPDIR/dist
 
 if [ $installer = "yes" ]; then
-  $SHELL ../makeinst-script.sh $OCTAVE_TARGET-$DATE
+  ../makeinst-script.sh $OCTAVE_TARGET-$DATE
 
   echo "Generating installer ..."
   $TOPDIR/usr/bin/$TARGET-makensis octave.nsi > /dev/null