diff options
| author | Son Ho | 2022-01-27 18:46:05 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-27 18:46:05 +0100 |
| commit | 88f5aa47d97b212fe9cc6187b818493d30a9db98 (patch) | |
| tree | f78ae018b4c9f7f5d2c7787774e3dfa2c47e9558 /dune-project | |
| parent | ea254c8af48ad5b4efd56624de40a9cb42452dd2 (diff) | |
Add a "basename" field in Pure.var
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions