diff options
| author | Hugo Herbelin | 2017-09-11 16:04:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-09-12 20:06:47 +0200 |
| commit | 712c0f124da2322dc58b012a110894329360581d (patch) | |
| tree | 78ddfa3b66fe7bcc69740bf677a81cbee9f79a2f /API/API.mli | |
| parent | cc94172036789cfef28007f59510b7f17df5d45d (diff) | |
Removing now useless former fix to #3333 (check valid module names).
The fix is not anymore needed after Id.of_string was made strict
(5b218f87). This allows to support the whole official syntax of
identifiers and not just the alpha-numerical ones (without quote).
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions