From 5ced22296292f6e47a3161ceaeedc5bf603b52e9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Chapoton?= Date: Tue, 25 Apr 2023 21:17:15 +0200 Subject: [PATCH] using -name in sage-grep --- src/bin/sage-grep | 2 +- src/bin/sage-grepdoc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/bin/sage-grep b/src/bin/sage-grep index b5161f365b3..c7975ae97af 100755 --- a/src/bin/sage-grep +++ b/src/bin/sage-grep @@ -2,4 +2,4 @@ cd "$SAGE_SRC" -find sage -print | GREP_OPTIONS= grep -E '.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 795bcfaaa75..ee6dff707e2 100755 --- a/src/bin/sage-grepdoc +++ b/src/bin/sage-grepdoc @@ -2,4 +2,4 @@ cd "$SAGE_DOC" -find html -print | GREP_OPTIONS= grep -E '.html$' | xargs grep "$@" +find html -name '*.html' | xargs grep "$@"