Deleting post does not delete report notifications

Deleting a post which has been reported causes the report to also be deleted, but leaves behind "Post reported" notifications, which link to non-existent posts/reports. This does not happen if the report is deleted before deleting the post.

Adding 'notification.type.report_post' to the $delete_notifications_types array in function delete_posts() (functions_admin.php) appears to solve this problem.

I was able to work around the issue by making this change via the core.delete_posts_after event in an extension.