diff options
| author | Pierre-Marie Pédrot | 2020-07-02 12:52:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-07-02 12:52:25 +0200 |
| commit | 2fc9f27449ed21f2cbb440b4684a56622cb2d064 (patch) | |
| tree | f81f2464fca70884cd17082a1e6a3d87e5380a21 /lib/objFile.mli | |
| parent | b017e302f69f20fc4fc3d4088a305194f6c387fa (diff) | |
| parent | 36faebc29986f7e895a7de16c6f2ea4c5b6fd074 (diff) | |
Merge PR #12618: Use weak ref to memoize Evarutil.is_ground_env
Reviewed-by: ppedrot
Diffstat (limited to 'lib/objFile.mli')
0 files changed, 0 insertions, 0 deletions