lint: exception for fix_leveldb_ptrarith_pr31671

This commit is contained in:
Luke Dashjr 2025-02-17 15:18:13 +00:00
parent 19e8086b9f
commit 248c26411d

View File

@ -111,6 +111,7 @@ echo "$DIR in $COMMIT was last updated in commit $old (tree $tree_commit)"
if [ "$tree_actual_tree" != "$tree_commit" ]; then
git diff "$tree_commit" "$tree_actual_tree" >&2
echo "FAIL: subtree directory was touched without subtree merge" >&2
[ "$DIR:$old" = "src/leveldb:a37778d4d32b4ddeff96f68a130dc8da3a84b278" ] || # exception
exit 1
fi