From dbb60b312f137979284cb123d17a0a0729bf3922 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 30 Oct 2002 15:29:30 +0000
Subject: [PATCH] Minor interface improvement.

---
 helm/gTopLevel/gTopLevel.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index e5ad5973e..85f56c155 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -1267,7 +1267,9 @@ let searchPattern rendering_window () =
             " <h1>Objects that can actually be applied: </h1> " ^
             String.concat "<br>" uris' ^ exc ^
             " <h1>Number of false matches: " ^
-             string_of_int (List.length uris - List.length uris') ^ "</h1>"
+             string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
+            " <h1>Number of good matches: " ^
+             string_of_int (List.length uris') ^ "</h1>"
            in
             output_html outputhtml html' ;
             let uri' = user_uri_choice uris' in
-- 
2.39.2