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

[helm.git] / components / binaries / transcript / grafite.ml

diff --git a/components/binaries/transcript/grafite.ml b/components/binaries/transcript/grafite.ml
index 1b8c640f87b180be16a3263d05345ede09eb7967..93bd922ef3f0294631cbbfa35cff6f8385941559 100644 (file)
--- a/components/binaries/transcript/grafite.ml
+++ b/components/binaries/transcript/grafite.ml
@@ -63,7 +63,7 @@ let out_command och cmd =
    let term_pp = NP.pp_term in
    let lazy_term_pp = NP.pp_term in
    let obj_pp = NP.pp_obj NP.pp_term in
-   let s = GP.pp_statement ~term_pp ~lazy_term_pp ~obj_pp cmd in
+   let s = GP.pp_statement ~map_unicode_to_tex:false ~term_pp ~lazy_term_pp ~obj_pp cmd in
    Printf.fprintf och "%s\n\n" s
 
 let command_of_obj obj =