From 9a2abbe9b8b7bebc6427991a28fc41f9a51d9609 Mon Sep 17 00:00:00 2001
From: M Somerville <matthew-github@dracos.co.uk>
Date: Fri, 19 Feb 2021 15:42:57 +0000
Subject: [PATCH] Fix error message reporting deleted annotation.

---
 www/docs/report/index.php | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/www/docs/report/index.php b/www/docs/report/index.php
index df8cb3b8cb..ef15ffec59 100644
--- a/www/docs/report/index.php
+++ b/www/docs/report/index.php
@@ -20,7 +20,10 @@
 
     if ($COMMENT->exists() == false || !$COMMENT->visible()) {
         // This comment id didn't exist in the DB.
-        trigger_error("There is no annotation with an ID of '" . _htmlentities($comment_id) . "'.", E_USER_NOTICE);
+        $PAGE->error_message("There is no annotation with that ID");
+        $PAGE->stripe_end();
+        $PAGE->page_end();
+        exit;
     }
 
     // OK, we've got a valid comment ID.