map_unicode_to_tex is no longer optional and it always refers to the current

[helm.git] / matita / matita.ml

diff --git a/matita/matita.ml b/matita/matita.ml
index 5873b22514e252da8579d6a890150ce9c8eb46ec..58d404888d7bde1e178185eaf21833651518689b 100644 (file)
--- a/matita/matita.ml
+++ b/matita/matita.ml
@@ -174,6 +174,8 @@ let _ =
        (fun _ -> 
         prerr_endline 
           (ApplyTransformation.txt_of_cic_object 120 GrafiteAst.Declarative "" 
+            ~map_unicode_to_tex:(Helm_registry.get_bool
+              "matita.paste_unicode_as_tex")
             (match 
             (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status
             with