Merge pull request #11529 from phire/egrep

lint: replace egrep with grep -E
This commit is contained in:
Pierre Bourdon 2023-02-02 05:33:35 +01:00 committed by GitHub
commit 6cb8df7658
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -103,17 +103,17 @@ function java_check() {
# Loop through each modified file.
for f in ${modified_files}; do
# Filter them.
if echo "${f}" | egrep -q "[.]java$"; then
if echo "${f}" | grep -E -q "[.]java$"; then
# Copy Java files to a temporary directory
java_setup
mkdir -p $(dirname "${java_temp_dir}/${f}")
cp "${f}" "${java_temp_dir}/${f}"
continue
fi
if ! echo "${f}" | egrep -q "[.](cpp|h|mm)$"; then
if ! echo "${f}" | grep -E -q "[.](cpp|h|mm)$"; then
continue
fi
if ! echo "${f}" | egrep -q "^Source"; then
if ! echo "${f}" | grep -E -q "^Source"; then
continue
fi