diff options
author | Son Ho | 2022-01-07 11:19:26 +0100 |
---|---|---|
committer | Son Ho | 2022-01-07 11:19:26 +0100 |
commit | 37bcc5a38cf7d92d70c16850714b42d57846c7c2 (patch) | |
tree | 2ab049583a02ddd363f6f5e586c2ca6914229c9b /src/InterpreterBorrowsCore.ml | |
parent | e41b8da810b80a3e42bd5289dedfdb7bf2f10550 (diff) |
Add logging information for borrows
Diffstat (limited to 'src/InterpreterBorrowsCore.ml')
-rw-r--r-- | src/InterpreterBorrowsCore.ml | 3 |
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... *) |