diff options
| author | Hugo Herbelin | 2018-10-09 21:08:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-19 16:56:08 +0200 |
| commit | 2e53939f4ce4bc06a5e7b621bc560d3ebeb59110 (patch) | |
| tree | fa55c604fcd8651ecc2fd40fd797ad078f71c03f /library/libobject.mli | |
| parent | 9b5ceabc9b62cdf9b806bb4abdff73642113e12e (diff) | |
Deprecating unused Engine.type_of_global.
Diffstat (limited to 'library/libobject.mli')
0 files changed, 0 insertions, 0 deletions