diff options
| author | Tristan Riehs <tristan.riehs@inria.fr> | 2025-12-29 13:09:05 +0100 |
|---|---|---|
| committer | Tristan Riehs <tristan.riehs@inria.fr> | 2025-12-29 13:09:05 +0100 |
| commit | 8afdb2d8afced8c5ec1ee49472f731dd3eab0bda (patch) | |
| tree | e6f4398ce3b4298907a22c64d05fd3ce864723a1 /src/Makefile | |
| parent | 6b584537838dbce9d3d75b93228544cee6e2f805 (diff) | |
Add file extensions to database
I chose to kind of abstract the extensions. Thus they are not part of
files' full and canonical names. However, they have to be there when
exporting the files so we need to store them somewhere.
Diffstat (limited to 'src/Makefile')
0 files changed, 0 insertions, 0 deletions