+2012-11-06 Pierre Muller <muller@sourceware.org>
+
+ * contrib/ari/create-web-ari-in-src.sh: Avoid problem if script
+ is not executable.
+
2012-11-05 Joel Brobecker <brobecker@adacore.com>
* gnulib/update-gnulib.sh: New script.
fi
# Launch update-web-ari.sh in same directory as current script.
-${scriptpath}/update-web-ari.sh ${srcdir} ${tempdir} ${webdir} gdb
+${SHELL} ${scriptpath}/update-web-ari.sh ${srcdir} ${tempdir} ${webdir} gdb
if [ -f "${webdir}/index.html" ] ; then
echo "ARI output can be viewed in file \"${webdir}/index.html\""