diff options
| author | Gaëtan Gilbert | 2019-05-05 16:32:17 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-04 09:33:41 +0200 |
| commit | 1bf2a088387949c13602997d181e6f7d0f014b3f (patch) | |
| tree | da3a1fd1289f57efa3a9ea33f345581c1145594c /doc/plugin_tutorial/tuto3/src | |
| parent | a18b1ae63e07cf7e174e3e8862ac32f00ce74865 (diff) | |
rewrite.ml: drop the id returned by new_instance earlier
We never use this id in rewrite.ml so don't bother threading it around.
Diffstat (limited to 'doc/plugin_tutorial/tuto3/src')
0 files changed, 0 insertions, 0 deletions