]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/interface/mmlinterface.ml
The interface sorts the entryes in the trees
[helm.git] / helm / interface / mmlinterface.ml
index 76f6e5a78940b291aefc4d8905bf5f6aa8ff19b9..d364ffe4b0257efbff9d48eb0da54a8742f83741 100755 (executable)
@@ -385,7 +385,7 @@ let mktree selection_changed rendering_window =
              ignore(treeitem2#connect#select
               (selection_changed rendering_window uri)) ;
              aux treeitem2 ti
-         ) !content
+         ) (List.sort compare !content)
    | _ -> ()
  in
   aux