From 38eab3e54a5bbcb2d064d0ef504e8584a33486bb Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 30 Apr 2021 18:37:48 +0200
Subject: [PATCH] [Release] remove usage of rgrep
---
doc/release/build.tex | 2 +-
doc/release/checktar.sh | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/doc/release/build.tex b/doc/release/build.tex
index 4eec599e4e4..39eed3e2cf7 100644
--- a/doc/release/build.tex
+++ b/doc/release/build.tex
@@ -7,10 +7,10 @@ The procedure for creating the source distribution.
\begin{itemize}
\item All tools needed to compile Frama-C (that you should have anyways)
\item \texttt{bash} v4.0 or higher
-\item \texttt{rgrep}
\item \texttt{git-lfs}
\item GNU \texttt{parallel}
\item a \TeX distribution
+\item \texttt{latexmk}
\item (recommended) \texttt{texfot}
\end{itemize}
diff --git a/doc/release/checktar.sh b/doc/release/checktar.sh
index 66a852c693b..171c33f7819 100755
--- a/doc/release/checktar.sh
+++ b/doc/release/checktar.sh
@@ -32,7 +32,7 @@ do
fi
done
-RESULT=$(rgrep $HOME $DIR)
+RESULT=$(grep -Iir $HOME $DIR)
if [[ "$RESULT" != "" ]]; then
echo "### ERROR: Found some $HOME occurrences in the distribution"
--
GitLab