using -name in sage-grep

fchapoton · fchapoton · commit 5ced22296292 · 2023-04-25T21:17:15.000+02:00
diff --git 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
@@ -2,4 +2,4 @@
 
 cd "$SAGE_DOC"
 
-find html -print | GREP_OPTIONS= grep -E '.html$' | xargs grep "$@"
+find html -name '*.html' | xargs grep "$@"

Original file line number	Diff line number	Diff line change
`@@ -2,4 +2,4 @@`
`2`	`2`
`3`	`3`	`cd "$SAGE_SRC"`
`4`	`4`
`5`		`-find sage -print \| GREP_OPTIONS= grep -E '.py([xdi])?$' \| xargs grep "$@"`
	`5`	`+find sage -name ".py" -o -name ".pyx" -o -name ".pxi" -o -name ".pxd" \| xargs grep "$@"`
Original file line number	Diff line number	Diff line change
`@@ -2,4 +2,4 @@`
`2`	`2`
`3`	`3`	`cd "$SAGE_DOC"`
`4`	`4`
`5`		`-find html -print \| GREP_OPTIONS= grep -E '.html$' \| xargs grep "$@"`
	`5`	`+find html -name '*.html' \| xargs grep "$@"`