diff options
| author | Son Ho | 2023-10-26 14:37:34 +0200 |
|---|---|---|
| committer | Son Ho | 2023-10-26 14:37:34 +0200 |
| commit | 005ad3cc03745bc9211defa481d5e45738a6d832 (patch) | |
| tree | f2854b27143dc2d602ce4f07ad9c28c7f775a62a /.gitignore | |
| parent | c380ab1699a115edf88e9d83234a4423333e52bf (diff) | |
Improve the handling of saved function effects in ExtractBuiltin.ml
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions