Merge pull request #206 from FStarLang/vdum_js_print

Set custom JS printer function in loader
FStarLang · Apr 29, 2021 · 55c83e7 · 55c83e7
2 parents 6e60e33 + 84f4c38
commit 55c83e7
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/kremlib/js/loader.js b/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,