Merge branch 'dev'3.5.0

1 files changed, 16 insertions, 0 deletions

diff --git a/coverage.sh b/coverage.sh
new file mode 100755
index 00000000..6d1362a8
--- /dev/null
+++ b/coverage.sh
@@ -0,0 +1,16 @@
+#!/bin/sh
+
+set -e
+
+objdir=$1
+suffix=$2
+shift 2
+objs=$@
+
+gcov -b -p -f -o "${objdir}" ${objs}
+
+# Move gcov outputs so that subsequent gcov invocations won't clobber results
+# for the same sources with different compilation flags.
+for f in `find . -maxdepth 1 -type f -name '*.gcov'` ; do
+  mv "${f}" "${f}.${suffix}"
+done