diff --git a/doc/release/build.tex b/doc/release/build.tex index 4eec599e4e42c8d1ccad4ed6bfb54aaa28499902..39eed3e2cf78c9e60d2702dea5cc7cb74376540e 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 66a852c693bcc02af7e3a92ea51fd9bbdef5c5e1..171c33f7819471e25cd9c4f2a9b83c39395e36b4 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"