diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-22 00:49:36 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-22 00:49:36 +0100 |
| commit | 051ef20a9f9c496fc6a5143de97450ccf7786c5b (patch) | |
| tree | b298a34e49450cbff00ac4341d7d64cbac8e537a /ide/ideutils.mli | |
| parent | 151286ec0c0887d212e7e85205352de4ddbf4bf2 (diff) | |
| parent | addc1304de75800fa9301e97d3ae78539f511959 (diff) | |
Merge PR#478: Small optimization on handling of library state.
Diffstat (limited to 'ide/ideutils.mli')
0 files changed, 0 insertions, 0 deletions