diff options
| author | Pierre-Marie Pédrot | 2014-05-11 16:48:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-11 16:48:56 +0200 |
| commit | 80b23d020c938a2c06654c8bb0cd15c806e6a582 (patch) | |
| tree | eaa38aa26ec23a8fab216858b9e7229fded9f44f /plugins | |
| parent | 064be83a050015ec3897867ca307ef494de30e67 (diff) | |
Using Maps to handle imports in Safe_typing. The order is irrelevant indeed,
and the lookup operation proved to be costly when dealing with big libraries.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions