.github: ensure there is no change after make-fix

Signed-off-by: Wei Fu <fuweid89@gmail.com>
This commit is contained in:
Wei Fu 2023-09-30 17:35:14 +08:00
parent da9248d2fd
commit 0ece40453a

View File

@ -30,3 +30,13 @@ jobs:
set -euo pipefail
make fix
DIFF=$(git status --porcelain)
if [ -n "$DIFF" ]; then
echo "These files were modified:"
echo
echo "$DIFF"
echo
exit 1
fi