]> matita.cs.unibo.it Git - helm.git/commitdiff
* the type of the constructor was wrong
authorLuca Padovani <luca.padovani@unito.it>
Wed, 12 Feb 2003 16:24:58 +0000 (16:24 +0000)
committerLuca Padovani <luca.padovani@unito.it>
Wed, 12 Feb 2003 16:24:58 +0000 (16:24 +0000)
helm/DEVEL/mathml_editor/ocaml/i_mathml_editor.ml

index 5019fbeff62fc351da1b4cf3f996552be7f5d04b..f3ca57454533f90b13f63fc30a880ca9c5e154c9 100644 (file)
@@ -5,7 +5,7 @@ external create :
   dictionary:[> `Document] GdomeT.t ->
   mml: [> `Document] GdomeT.t -> 
   tex: [> `Document] GdomeT.t ->
-  log:(string -> unit) ->
+  log:(int -> string -> unit) ->
   t
   = "ml_mathml_editor_new"