From 72e4059f7141d5cdf573e470e9858a0e68d6fceb Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 8 Jun 2005 16:06:47 +0000
Subject: [PATCH] Query results were erroneously tagged as directories.
---
helm/matita/matitaMathView.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index dc90df9db..6db20400e 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -471,7 +471,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
| `Uri uri -> self#_loadUriManagerUri (UriManager.uri_of_string uri)
| `Whelp (query, results) ->
set_whelp_query query;
- self#_loadList (List.map (fun r -> "dir", r) results));
+ self#_loadList (List.map (fun r -> "obj", r) results));
self#setEntry entry
end
with
--
2.39.2