From 25f1d458b2d5bbde29b87d59c1307671e82ed2c9 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 28 Apr 2021 15:39:25 +0200
Subject: [PATCH] [Distrib] Use grep instead of rgrep
---
bin/build-src-distrib.sh | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/bin/build-src-distrib.sh b/bin/build-src-distrib.sh
index cb6ce24f3d0..cc070b874d3 100755
--- a/bin/build-src-distrib.sh
+++ b/bin/build-src-distrib.sh
@@ -23,9 +23,9 @@ if ! command -v git-lfs >/dev/null 2>/dev/null; then
exit 99
fi
-# rgrep needs to be installed
-if ! command -v rgrep --version >/dev/null 2>/dev/null; then
- echo "rgrep is required"
+# grep needs to be installed
+if ! command -v grep --version >/dev/null 2>/dev/null; then
+ echo "grep is required"
exit 99
fi
@@ -100,7 +100,7 @@ function look_for_uncommited_changes {
}
function look_for_frama_c_dev {
- rgrep -i "frama-c+dev" src &> /dev/null
+ grep -Iir "frama-c+dev" src &> /dev/null
if [ "$?" == "0" ]; then
echo "### WARNING: Remaining frama-c+dev occurrences in 'src'"
proceed_anyway "Update API, then run the script again"
--
GitLab