Eureka!

[helm.git] / helm / gTopLevel / chosenTermEditor.ml

diff --git a/helm/gTopLevel/chosenTermEditor.ml b/helm/gTopLevel/chosenTermEditor.ml
index f6a7b0380e6f39676c0f4e50adaf4d53632371ba..25dcfd2e52b3bd5abb157555a2ffadf483396c87 100644 (file)
--- a/helm/gTopLevel/chosenTermEditor.ml
+++ b/helm/gTopLevel/chosenTermEditor.ml
@@ -1,7 +1,4 @@
+include TermEditor
 (*
-module ChosenTermEditor  = TexTermEditor;;
+include TexTermEditor
 *)
-module ChosenTermEditor = TermEditor;;
-
-module Make = ChosenTermEditor.Make;;
-class type term_editor = ChosenTermEditor.term_editor;;