diff options
| author | Hugo Herbelin | 2017-09-21 17:08:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-09-21 17:54:38 +0200 |
| commit | dc5b8f1793c6f7104f0b4762d9887be255709ead (patch) | |
| tree | f30002a972f425295b98df3098686a0946091480 /API/API.mli | |
| parent | 95400806e85aaea109740e8fa77c0edb9f8b7a09 (diff) | |
Proposing meta names more distinguishable from evar names than ?M42.
Using "?INTERNAL#42" with a # to emphasize a meaningless re-parsability.
Tough maybe it signals too much an unelegant debugging flavor?
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions