diff options
| author | Son Ho | 2024-04-04 16:08:32 +0200 |
|---|---|---|
| committer | Son Ho | 2024-04-04 16:08:32 +0200 |
| commit | 4828b77847ee981f5c6a1bbad7f8e6ed0e58eb0f (patch) | |
| tree | 89f6a530a6c251d62156d7c84307c4d316d8ceb3 /backends/fstar/Makefile | |
| parent | 7f7387c5519da00133ad557450695e6d6838f93c (diff) | |
Rename Result.ret as Result.ok in the backends
Diffstat (limited to 'backends/fstar/Makefile')
0 files changed, 0 insertions, 0 deletions