Skip to content

Commit

Permalink
Update Makefile
Browse files Browse the repository at this point in the history
  • Loading branch information
weizhoublue authored Jul 29, 2023
1 parent 5cd5d99 commit a4edd38
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -394,7 +394,7 @@ check_doc:
echo "!!! error, failed to build doc" ; \
exit 1 ; \
fi ; \
if grep -E "WARNING .* contains a link to .* which is not found" <<< "$${MESSAGE}" ; then \
if grep -E "WARNING .* which is not found" <<< "$${MESSAGE}" ; then \
echo "!!! error, some link is bad" ; \
exit 1 ; \
fi
Expand Down

0 comments on commit a4edd38

Please sign in to comment.