diff options
| author | Emilio Jesus Gallego Arias | 2019-07-15 15:27:53 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-15 15:27:53 +0200 |
| commit | 19b92fb6767b0f9c84ea7d6331d764269734a883 (patch) | |
| tree | 5ccad6b24a1084d608b08aaddd06768d00d256d2 /doc/plugin_tutorial/tuto1/src/simple_print.ml | |
| parent | a5998b06ccf2367f7d1e58dc80e4237754c953bc (diff) | |
[funind] Remove unneeded callback.
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_print.ml')
0 files changed, 0 insertions, 0 deletions