Merge branch 'master' into matthiaskrgr/all_grep

diff --git a/misc/tools/all/git.subr b/misc/tools/all/git.subr
index 69ad888f10faf3b5f84f8d7297213ba82a1b55a6..cf19f7589465b2e0b3cfc35e097582cb9b107e37 100644 (file)
--- a/misc/tools/all/git.subr
+++ b/misc/tools/all/git.subr
@@ -960,6 +960,14 @@ case "$cmd" in
                $ECHO "  $SELF update|pull [-N] [-s | -h [-p] | -g [-p]] [-l de|nl|default]"
                handled=false
                ;;
+       grep)
+               for d in $repos; do
+                       if verbose cd "$d0/$d"; then
+                               git grep -I "$@" || true
+                               cd "$d0"
+                       fi
+               done
+               ;;
        *)
                handled=false
                ;;