Minor interface improvement.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index e5ad5973e6af05a67fb3be44640171e666933eb7..85f56c1558fd1c9d108e4fd25417c07fddad0c8d 100644 (file)
--- 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