diff --git a/src/bin/sage-grep b/src/bin/sage-grep index 8441fa83519..c7975ae97af 100755 --- a/src/bin/sage-grep +++ b/src/bin/sage-grep @@ -2,4 +2,4 @@ cd "$SAGE_SRC" -find sage -print | GREP_OPTIONS= egrep '.py([xdi])?$' | xargs grep "$@" +find sage -name "*.py" -o -name "*.pyx" -o -name "*.pxi" -o -name "*.pxd" | xargs grep "$@" diff --git a/src/bin/sage-grepdoc b/src/bin/sage-grepdoc index ec0383178ed..ee6dff707e2 100755 --- a/src/bin/sage-grepdoc +++ b/src/bin/sage-grepdoc @@ -2,4 +2,4 @@ cd "$SAGE_DOC" -find html -print | GREP_OPTIONS= egrep '.html$' | xargs grep "$@" +find html -name '*.html' | xargs grep "$@"