Merge branch 'dev'5.0.0

1 files changed, 0 insertions, 16 deletions

diff --git a/coverage.sh b/coverage.sh
deleted file mode 100755
index 6d1362a..0000000
--- a/coverage.sh
+++ /dev/null
@@ -1,16 +0,0 @@
-#!/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