Merge branch 'master' of pro.github.com:FStarLang/kremlin

FStarLang · May 5, 2021 · 4e48d26 · 4e48d26
2 parents 6c69788 + 55c83e7
commit 4e48d26
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,