diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-09-29 17:45:27 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-09-29 17:45:27 +0200 |
| commit | 05ab666a1283de5500dbc0520d18bdb05d95f286 (patch) | |
| tree | 538cb7b07372d4e83a6c7823d5cb59ee54606099 /library/loadpath.ml | |
| parent | 82a618e8a4945752698a7900c8af7a51091f7b1b (diff) | |
Make the interface of System.raw_extern_intern much saner.
There is no reason (any longer?) to create simultaneous closures for
interning and externing files. This patch makes the code more readable
by separating both functions and their signatures.
Diffstat (limited to 'library/loadpath.ml')
0 files changed, 0 insertions, 0 deletions