X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2FmatitaWiki.ml;h=3c5607bd7df9ff1bf458d61f5f0dac65a3aea604;hb=c68d9805aa7e37554bc4f00eca61083b75ef43da;hp=bbe8d2ed7247f60132ffa0f97e4c7e298959efc9;hpb=871d9b1d66f79445e7afa6d42205aaf33576c4f0;p=helm.git diff --git a/matita/matitaWiki.ml b/matita/matitaWiki.ml index bbe8d2ed7..3c5607bd7 100644 --- a/matita/matitaWiki.ml +++ b/matita/matitaWiki.ml @@ -167,6 +167,8 @@ let rec interactive_loop () = (List.map (fun i -> ApplyTransformation.txt_of_cic_sequent 80 metasenv + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") (List.find (fun (j,_,_) -> j=i) metasenv) ) open_goals)) | _ -> ()