Merge remote branch 'asp/master'

Conflicts:
	bin/git-update.sh

diff --git a/bin/git-update.sh b/bin/git-update.sh
index 3fea2d6a7bf0c0fbefadf435d33da300957d4797..de71bec0dc304c78b3041bd13ae85228642f05a1 100755 (executable)
--- a/bin/git-update.sh
+++ b/bin/git-update.sh
@@ -27,6 +27,7 @@ if [ x$LOCAL = x ]; then
     # Push all local changes to remote(s).
     for remote in `git remote`; do
         git push $remote 2>&1 | grep -v 'Everything up-to-date'
+        git push --tags $remote 2>&1 | grep -v 'Everything up-to-date'
     done
 fi
 # Show unmerged changes.

diff --git a/bin/valgrind-ptr.sh b/bin/valgrind-ptr.sh
new file mode 100755 (executable)
index 0000000..965a587
--- /dev/null
+++ b/bin/valgrind-ptr.sh
@@ -0,0 +1,3 @@
+#!/bin/sh
+
+valgrind --tool=exp-ptrcheck --error-exitcode=1 "$@"

diff --git a/bin/valgrind.sh b/bin/valgrind.sh
new file mode 100755 (executable)
index 0000000..dd8038a
--- /dev/null
+++ b/bin/valgrind.sh
@@ -0,0 +1,3 @@
+#!/bin/sh
+
+valgrind --leak-check=full --show-reachable=yes --error-exitcode=1 "$@"