diff options
| author | Son Ho | 2023-11-24 17:10:05 +0100 |
|---|---|---|
| committer | Son Ho | 2023-11-24 17:10:05 +0100 |
| commit | 5b9f8de676829817d2b776166fda66bfb5128d6c (patch) | |
| tree | fd6b73e1a0f5e8c916b2f58ce1afe5bde6e4838a /tests/fstar/.gitignore | |
| parent | 1b446285bbbe356ead7c0e521799b35020f08147 (diff) | |
Improve the error messages for some name collisions
Diffstat (limited to 'tests/fstar/.gitignore')
0 files changed, 0 insertions, 0 deletions