summaryrefslogtreecommitdiff
path: root/src/InterpreterBorrowsCore.ml
diff options
context:
space:
mode:
authorSon Ho2022-01-07 11:19:26 +0100
committerSon Ho2022-01-07 11:19:26 +0100
commit37bcc5a38cf7d92d70c16850714b42d57846c7c2 (patch)
tree2ab049583a02ddd363f6f5e586c2ca6914229c9b /src/InterpreterBorrowsCore.ml
parente41b8da810b80a3e42bd5289dedfdb7bf2f10550 (diff)
Add logging information for borrows
Diffstat (limited to 'src/InterpreterBorrowsCore.ml')
-rw-r--r--src/InterpreterBorrowsCore.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index bc2f5971..aaab18cb 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -9,6 +9,9 @@ module Subst = Substitute
module L = Logging
open InterpreterUtils
+(** The local logger *)
+let log = L.borrows_log
+
(** TODO: cleanup this a bit, once we have a better understanding about
what we need.
TODO: I'm not sure in which file this should be moved... *)