diff options
| author | Hugo Herbelin | 2020-08-31 12:20:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-10 23:19:32 +0200 |
| commit | 5ef7598009bf49feafd632c0171a1bb14bef6448 (patch) | |
| tree | 03f0bd061305f71864d7c3a4df73144ccb25ba17 /interp | |
| parent | 8d27b12365a1d8b3f1670a055537dd3724583baf (diff) | |
Adding a warning in case a notation is used neither for parsing nor printing.
Diffstat (limited to 'interp')
0 files changed, 0 insertions, 0 deletions