diff options
author | Son Ho | 2022-01-12 20:37:08 +0100 |
---|---|---|
committer | Son Ho | 2022-01-12 20:37:08 +0100 |
commit | 7ddb32b347c56c98d81b3584f5a53bfeff284c01 (patch) | |
tree | a2e7797d10c3b73301452ce62b955a931a315351 /src/InterpreterStatements.ml | |
parent | 8d39d5a50141ba5addac685be2653da7a9f95c8d (diff) |
Remove the inner_outer parameter from end_borrow, etc.
Diffstat (limited to 'src/InterpreterStatements.ml')
0 files changed, 0 insertions, 0 deletions