diff options
| author | Emilio Jesus Gallego Arias | 2018-09-18 20:11:41 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-18 20:11:41 +0200 |
| commit | 65a5d6ce9a7a3c35bd426b7e5dcc88cb35f498b1 (patch) | |
| tree | 42cd98c5603025131c388ffd454093b4c1563089 /kernel/nativelambda.ml | |
| parent | 15649c16bc4e20ef2c2b1b0ac645f83ee03c3589 (diff) | |
[api] Deprecate two forgotten print functions that use global state.
Removal of the global state API is scheduled for 8.10, thus it is
crucial we ship this in 8.9.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions