1) Matitaweb now disambiguates scripts as it runs them

[helm.git] / matitaB / matita / matitaEngine.ml

diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml
index aa271b2a1ca948b69ae67c3c008fd871e479fb59..48ff2d360dc5394ba01ee090540fa899c3807baa 100644 (file)
--- a/matitaB/matita/matitaEngine.ml
+++ b/matitaB/matita/matitaEngine.ml
@@ -240,7 +240,9 @@ and compile ~compiling ~asserted ~include_paths ~outch ?uid fname =
      (* XXX: update script -- currently to stdout *)
      let origbuf = Ulexing.from_utf8_channel (open_in fname) in
      let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in
-     ignore (SmallLexer.mk_small_printer interpr outch origbuf);
+     let outstr = ref "" in
+     ignore (SmallLexer.mk_small_printer interpr outstr origbuf);
+     Printf.fprintf outch "%s" !outstr;
      asserted
 (* MATITA 1.0: debbo fare time_travel sulla ng_library?
      LexiconSync.time_travel