diff options
| author | Hugo Herbelin | 2020-08-30 18:12:09 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-10 17:22:48 +0200 |
| commit | a2733be481563faff6505dd975a0a067ce28722a (patch) | |
| tree | b9457a898d2f72853ed3faec8a09f10fa945ca40 /dev/base_include | |
| parent | a764c64bfe3d3c604931087459fb6f4ae727cbea (diff) | |
When a notation is only parsing, do not attach to it a specific format.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions