diff options
| author | Ryan Lahfa | 2024-05-13 18:10:39 +0200 |
|---|---|---|
| committer | Ryan Lahfa | 2024-05-13 18:10:39 +0200 |
| commit | 001f3553287a51c1704ea3033a44e548440ec108 (patch) | |
| tree | c24c553eafb29e2c4ab763aca16b450770654341 /.gitignore | |
| parent | 5c758f8b9b70288f3ef428c53122c75677255520 (diff) | |
backends/lean: repair definition of `core.mem.replace`
Oops, it is supposed to do something with the second argument!
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions