Skip to content
Snippets Groups Projects
Commit 38eab3e5 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[Release] remove usage of rgrep

parent cf5840cc
No related branches found
No related tags found
No related merge requests found
......@@ -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}
......
......@@ -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"
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment