Merge pull request #206 from FStarLang/vdum_js_print

Set custom JS printer function in loader

Author: victor-dumitrescu

kremlib/js/loader.js

@@ -477,8 +477,14 @@ function link(imports, modules) {
   return fold(i, modules);
 }
 
+function setMyPrint(f) {
+  my_print = f;
+  return;
+}
+
 if (typeof module !== "undefined")
   module.exports = {
+    setMyPrint: setMyPrint,
     link: link,
     reserve: reserve,
     dump: dump,